%!PS-Adobe-2.0
%%Creator: dvips(k) 5.86 Copyright 1999 Radical Eye Software
%%Title: dddmp-2.0.dvi
%%Pages: 10
%%PageOrder: Ascend
%%BoundingBox: 0 0 612 792
%%DocumentFonts: Times-Bold Times-Roman Courier Times-Italic Helvetica
%%EndComments
%DVIPSWebPage: (www.radicaleye.com)
%DVIPSCommandLine: dvips -t letter -f dddmp-2.0
%DVIPSParameters: dpi=600, compressed
%DVIPSSource:  TeX output 2002.12.11:0557
%%BeginProcSet: texc.pro
%!
/TeXDict 300 dict def TeXDict begin/N{def}def/B{bind def}N/S{exch}N/X{S
N}B/A{dup}B/TR{translate}N/isls false N/vsize 11 72 mul N/hsize 8.5 72
mul N/landplus90{false}def/@rigin{isls{[0 landplus90{1 -1}{-1 1}ifelse 0
0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{
landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize
mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[
matrix currentmatrix{A A round sub abs 0.00001 lt{round}if}forall round
exch round exch]setmatrix}N/@landscape{/isls true N}B/@manualfeed{
statusdict/manualfeed true put}B/@copies{/#copies X}B/FMat[1 0 0 -1 0 0]
N/FBB[0 0 0 0]N/nn 0 N/IEn 0 N/ctr 0 N/df-tail{/nn 8 dict N nn begin
/FontType 3 N/FontMatrix fntrx N/FontBBox FBB N string/base X array
/BitMaps X/BuildChar{CharBuilder}N/Encoding IEn N end A{/foo setfont}2
array copy cvx N load 0 nn put/ctr 0 N[}B/sf 0 N/df{/sf 1 N/fntrx FMat N
df-tail}B/dfs{div/sf X/fntrx[sf 0 0 sf neg 0 0]N df-tail}B/E{pop nn A
definefont setfont}B/Cw{Cd A length 5 sub get}B/Ch{Cd A length 4 sub get
}B/Cx{128 Cd A length 3 sub get sub}B/Cy{Cd A length 2 sub get 127 sub}
B/Cdx{Cd A length 1 sub get}B/Ci{Cd A type/stringtype ne{ctr get/ctr ctr
1 add N}if}B/id 0 N/rw 0 N/rc 0 N/gp 0 N/cp 0 N/G 0 N/CharBuilder{save 3
1 roll S A/base get 2 index get S/BitMaps get S get/Cd X pop/ctr 0 N Cdx
0 Cx Cy Ch sub Cx Cw add Cy setcachedevice Cw Ch true[1 0 0 -1 -.1 Cx
sub Cy .1 sub]/id Ci N/rw Cw 7 add 8 idiv string N/rc 0 N/gp 0 N/cp 0 N{
rc 0 ne{rc 1 sub/rc X rw}{G}ifelse}imagemask restore}B/G{{id gp get/gp
gp 1 add N A 18 mod S 18 idiv pl S get exec}loop}B/adv{cp add/cp X}B
/chg{rw cp id gp 4 index getinterval putinterval A gp add/gp X adv}B/nd{
/cp 0 N rw exit}B/lsh{rw cp 2 copy get A 0 eq{pop 1}{A 255 eq{pop 254}{
A A add 255 and S 1 and or}ifelse}ifelse put 1 adv}B/rsh{rw cp 2 copy
get A 0 eq{pop 128}{A 255 eq{pop 127}{A 2 idiv S 128 and or}ifelse}
ifelse put 1 adv}B/clr{rw cp 2 index string putinterval adv}B/set{rw cp
fillstr 0 4 index getinterval putinterval adv}B/fillstr 18 string 0 1 17
{2 copy 255 put pop}for N/pl[{adv 1 chg}{adv 1 chg nd}{1 add chg}{1 add
chg nd}{adv lsh}{adv lsh nd}{adv rsh}{adv rsh nd}{1 add adv}{/rc X nd}{
1 add set}{1 add clr}{adv 2 chg}{adv 2 chg nd}{pop nd}]A{bind pop}
forall N/D{/cc X A type/stringtype ne{]}if nn/base get cc ctr put nn
/BitMaps get S ctr S sf 1 ne{A A length 1 sub A 2 index S get sf div put
}if put/ctr ctr 1 add N}B/I{cc 1 add D}B/bop{userdict/bop-hook known{
bop-hook}if/SI save N @rigin 0 0 moveto/V matrix currentmatrix A 1 get A
mul exch 0 get A mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N/eop{
SI restore userdict/eop-hook known{eop-hook}if showpage}N/@start{
userdict/start-hook known{start-hook}if pop/VResolution X/Resolution X
1000 div/DVImag X/IEn 256 array N 2 string 0 1 255{IEn S A 360 add 36 4
index cvrs cvn put}for pop 65781.76 div/vsize X 65781.76 div/hsize X}N
/p{show}N/RMat[1 0 0 -1 0 0]N/BDot 260 string N/Rx 0 N/Ry 0 N/V{}B/RV/v{
/Ry X/Rx X V}B statusdict begin/product where{pop false[(Display)(NeXT)
(LaserWriter 16/600)]{A length product length le{A length product exch 0
exch getinterval eq{pop true exit}if}{pop}ifelse}forall}{false}ifelse
end{{gsave TR -.1 .1 TR 1 1 scale Rx Ry false RMat{BDot}imagemask
grestore}}{{gsave TR -.1 .1 TR Rx Ry scale 1 1 false RMat{BDot}
imagemask grestore}}ifelse B/QV{gsave newpath transform round exch round
exch itransform moveto Rx 0 rlineto 0 Ry neg rlineto Rx neg 0 rlineto
fill grestore}B/a{moveto}B/delta 0 N/tail{A/delta X 0 rmoveto}B/M{S p
delta add tail}B/b{S p tail}B/c{-4 M}B/d{-3 M}B/e{-2 M}B/f{-1 M}B/g{0 M}
B/h{1 M}B/i{2 M}B/j{3 M}B/k{4 M}B/w{0 rmoveto}B/l{p -4 w}B/m{p -3 w}B/n{
p -2 w}B/o{p -1 w}B/q{p 1 w}B/r{p 2 w}B/s{p 3 w}B/t{p 4 w}B/x{0 S
rmoveto}B/y{3 2 roll p a}B/bos{/SS save N}B/eos{SS restore}B end

%%EndProcSet
%%BeginProcSet: 8r.enc
% @@psencodingfile@{
%   author = "S. Rahtz, P. MacKay, Alan Jeffrey, B. Horn, K. Berry",
%   version = "0.6",
%   date = "22 June 1996",
%   filename = "8r.enc",
%   email = "kb@@mail.tug.org",
%   address = "135 Center Hill Rd. // Plymouth, MA 02360",
%   codetable = "ISO/ASCII",
%   checksum = "119     662    4424",
%   docstring = "Encoding for TrueType or Type 1 fonts to be used with TeX."
% @}
% 
% Idea is to have all the characters normally included in Type 1 fonts
% available for typesetting. This is effectively the characters in Adobe
% Standard Encoding + ISO Latin 1 + extra characters from Lucida.
% 
% Character code assignments were made as follows:
% 
% (1) the Windows ANSI characters are almost all in their Windows ANSI
% positions, because some Windows users cannot easily reencode the
% fonts, and it makes no difference on other systems. The only Windows
% ANSI characters not available are those that make no sense for
% typesetting -- rubout (127 decimal), nobreakspace (160), softhyphen
% (173). quotesingle and grave are moved just because it's such an
% irritation not having them in TeX positions.
% 
% (2) Remaining characters are assigned arbitrarily to the lower part
% of the range, avoiding 0, 10 and 13 in case we meet dumb software.
% 
% (3) Y&Y Lucida Bright includes some extra text characters; in the
% hopes that other PostScript fonts, perhaps created for public
% consumption, will include them, they are included starting at 0x12.
% 
% (4) Remaining positions left undefined are for use in (hopefully)
% upward-compatible revisions, if someday more characters are generally
% available.
% 
% (5) hyphen appears twice for compatibility with both ASCII and Windows.
% 
/TeXBase1Encoding [
% 0x00 (encoded characters from Adobe Standard not in Windows 3.1)
  /.notdef /dotaccent /fi /fl
  /fraction /hungarumlaut /Lslash /lslash
  /ogonek /ring /.notdef
  /breve /minus /.notdef 
% These are the only two remaining unencoded characters, so may as
% well include them.
  /Zcaron /zcaron 
% 0x10
 /caron /dotlessi 
% (unusual TeX characters available in, e.g., Lucida Bright)
 /dotlessj /ff /ffi /ffl 
 /.notdef /.notdef /.notdef /.notdef
 /.notdef /.notdef /.notdef /.notdef
 % very contentious; it's so painful not having quoteleft and quoteright
 % at 96 and 145 that we move the things normally found there down to here.
 /grave /quotesingle 
% 0x20 (ASCII begins)
 /space /exclam /quotedbl /numbersign
 /dollar /percent /ampersand /quoteright
 /parenleft /parenright /asterisk /plus /comma /hyphen /period /slash
% 0x30
 /zero /one /two /three /four /five /six /seven
 /eight /nine /colon /semicolon /less /equal /greater /question
% 0x40
 /at /A /B /C /D /E /F /G /H /I /J /K /L /M /N /O
% 0x50
 /P /Q /R /S /T /U /V /W
 /X /Y /Z /bracketleft /backslash /bracketright /asciicircum /underscore
% 0x60
 /quoteleft /a /b /c /d /e /f /g /h /i /j /k /l /m /n /o
% 0x70
 /p /q /r /s /t /u /v /w
 /x /y /z /braceleft /bar /braceright /asciitilde
 /.notdef % rubout; ASCII ends
% 0x80
 /.notdef /.notdef /quotesinglbase /florin
 /quotedblbase /ellipsis /dagger /daggerdbl
 /circumflex /perthousand /Scaron /guilsinglleft
 /OE /.notdef /.notdef /.notdef
% 0x90
 /.notdef /.notdef /.notdef /quotedblleft
 /quotedblright /bullet /endash /emdash
 /tilde /trademark /scaron /guilsinglright
 /oe /.notdef /.notdef /Ydieresis
% 0xA0
 /.notdef % nobreakspace
 /exclamdown /cent /sterling
 /currency /yen /brokenbar /section
 /dieresis /copyright /ordfeminine /guillemotleft
 /logicalnot
 /hyphen % Y&Y (also at 45); Windows' softhyphen
 /registered
 /macron
% 0xD0
 /degree /plusminus /twosuperior /threesuperior
 /acute /mu /paragraph /periodcentered
 /cedilla /onesuperior /ordmasculine /guillemotright
 /onequarter /onehalf /threequarters /questiondown
% 0xC0
 /Agrave /Aacute /Acircumflex /Atilde /Adieresis /Aring /AE /Ccedilla
 /Egrave /Eacute /Ecircumflex /Edieresis
 /Igrave /Iacute /Icircumflex /Idieresis
% 0xD0
 /Eth /Ntilde /Ograve /Oacute
 /Ocircumflex /Otilde /Odieresis /multiply
 /Oslash /Ugrave /Uacute /Ucircumflex
 /Udieresis /Yacute /Thorn /germandbls
% 0xE0
 /agrave /aacute /acircumflex /atilde
 /adieresis /aring /ae /ccedilla
 /egrave /eacute /ecircumflex /edieresis
 /igrave /iacute /icircumflex /idieresis
% 0xF0
 /eth /ntilde /ograve /oacute
 /ocircumflex /otilde /odieresis /divide
 /oslash /ugrave /uacute /ucircumflex
 /udieresis /yacute /thorn /ydieresis
] def

%%EndProcSet
%%BeginProcSet: texps.pro
%!
TeXDict begin/rf{findfont dup length 1 add dict begin{1 index/FID ne 2
index/UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll
exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]/Metrics
exch def dict begin Encoding{exch dup type/integertype ne{pop pop 1 sub
dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get div def}
ifelse}forall Metrics/Metrics currentdict end def[2 index currentdict
end definefont 3 -1 roll makefont/setfont cvx]cvx def}def/ObliqueSlant{
dup sin S cos div neg}B/SlantFont{4 index mul add}def/ExtendFont{3 -1
roll mul exch}def/ReEncodeFont{CharStrings rcheck{/Encoding false def
dup[exch{dup CharStrings exch known not{pop/.notdef/Encoding true def}
if}forall Encoding{]exch pop}{cleartomark}ifelse}if/Encoding exch def}
def end

%%EndProcSet
%%BeginProcSet: special.pro
%!
TeXDict begin/SDict 200 dict N SDict begin/@SpecialDefaults{/hs 612 N
/vs 792 N/ho 0 N/vo 0 N/hsc 1 N/vsc 1 N/ang 0 N/CLIP 0 N/rwiSeen false N
/rhiSeen false N/letter{}N/note{}N/a4{}N/legal{}N}B/@scaleunit 100 N
/@hscale{@scaleunit div/hsc X}B/@vscale{@scaleunit div/vsc X}B/@hsize{
/hs X/CLIP 1 N}B/@vsize{/vs X/CLIP 1 N}B/@clip{/CLIP 2 N}B/@hoffset{/ho
X}B/@voffset{/vo X}B/@angle{/ang X}B/@rwi{10 div/rwi X/rwiSeen true N}B
/@rhi{10 div/rhi X/rhiSeen true N}B/@llx{/llx X}B/@lly{/lly X}B/@urx{
/urx X}B/@ury{/ury X}B/magscale true def end/@MacSetUp{userdict/md known
{userdict/md get type/dicttype eq{userdict begin md length 10 add md
maxlength ge{/md md dup length 20 add dict copy def}if end md begin
/letter{}N/note{}N/legal{}N/od{txpose 1 0 mtx defaultmatrix dtransform S
atan/pa X newpath clippath mark{transform{itransform moveto}}{transform{
itransform lineto}}{6 -2 roll transform 6 -2 roll transform 6 -2 roll
transform{itransform 6 2 roll itransform 6 2 roll itransform 6 2 roll
curveto}}{{closepath}}pathforall newpath counttomark array astore/gc xdf
pop ct 39 0 put 10 fz 0 fs 2 F/|______Courier fnt invertflag{PaintBlack}
if}N/txpose{pxs pys scale ppr aload pop por{noflips{pop S neg S TR pop 1
-1 scale}if xflip yflip and{pop S neg S TR 180 rotate 1 -1 scale ppr 3
get ppr 1 get neg sub neg ppr 2 get ppr 0 get neg sub neg TR}if xflip
yflip not and{pop S neg S TR pop 180 rotate ppr 3 get ppr 1 get neg sub
neg 0 TR}if yflip xflip not and{ppr 1 get neg ppr 0 get neg TR}if}{
noflips{TR pop pop 270 rotate 1 -1 scale}if xflip yflip and{TR pop pop
90 rotate 1 -1 scale ppr 3 get ppr 1 get neg sub neg ppr 2 get ppr 0 get
neg sub neg TR}if xflip yflip not and{TR pop pop 90 rotate ppr 3 get ppr
1 get neg sub neg 0 TR}if yflip xflip not and{TR pop pop 270 rotate ppr
2 get ppr 0 get neg sub neg 0 S TR}if}ifelse scaleby96{ppr aload pop 4
-1 roll add 2 div 3 1 roll add 2 div 2 copy TR .96 dup scale neg S neg S
TR}if}N/cp{pop pop showpage pm restore}N end}if}if}N/normalscale{
Resolution 72 div VResolution 72 div neg scale magscale{DVImag dup scale
}if 0 setgray}N/psfts{S 65781.76 div N}N/startTexFig{/psf$SavedState
save N userdict maxlength dict begin/magscale true def normalscale
currentpoint TR/psf$ury psfts/psf$urx psfts/psf$lly psfts/psf$llx psfts
/psf$y psfts/psf$x psfts currentpoint/psf$cy X/psf$cx X/psf$sx psf$x
psf$urx psf$llx sub div N/psf$sy psf$y psf$ury psf$lly sub div N psf$sx
psf$sy scale psf$cx psf$sx div psf$llx sub psf$cy psf$sy div psf$ury sub
TR/showpage{}N/erasepage{}N/copypage{}N/p 3 def @MacSetUp}N/doclip{
psf$llx psf$lly psf$urx psf$ury currentpoint 6 2 roll newpath 4 copy 4 2
roll moveto 6 -1 roll S lineto S lineto S lineto closepath clip newpath
moveto}N/endTexFig{end psf$SavedState restore}N/@beginspecial{SDict
begin/SpecialSave save N gsave normalscale currentpoint TR
@SpecialDefaults count/ocount X/dcount countdictstack N}N/@setspecial{
CLIP 1 eq{newpath 0 0 moveto hs 0 rlineto 0 vs rlineto hs neg 0 rlineto
closepath clip}if ho vo TR hsc vsc scale ang rotate rwiSeen{rwi urx llx
sub div rhiSeen{rhi ury lly sub div}{dup}ifelse scale llx neg lly neg TR
}{rhiSeen{rhi ury lly sub div dup scale llx neg lly neg TR}if}ifelse
CLIP 2 eq{newpath llx lly moveto urx lly lineto urx ury lineto llx ury
lineto closepath clip}if/showpage{}N/erasepage{}N/copypage{}N newpath}N
/@endspecial{count ocount sub{pop}repeat countdictstack dcount sub{end}
repeat grestore SpecialSave restore end}N/@defspecial{SDict begin}N
/@fedspecial{end}B/li{lineto}B/rl{rlineto}B/rc{rcurveto}B/np{/SaveX
currentpoint/SaveY X N 1 setlinecap newpath}N/st{stroke SaveX SaveY
moveto}N/fil{fill SaveX SaveY moveto}N/ellipse{/endangle X/startangle X
/yrad X/xrad X/savematrix matrix currentmatrix N TR xrad yrad scale 0 0
1 startangle endangle arc savematrix setmatrix}N end

%%EndProcSet
TeXDict begin 40258431 52099146 1000 600 600 (dddmp-2.0.dvi)
@start /Fa 143[55 1[55 7[28 2[50 99[{TeXBase1Encoding ReEncodeFont}4
99.6264 /Helvetica rf
%DVIPSBitmapFont: Fb cmr12 12 3
/Fb 3 53 df<14FF010713E090381F81F890383E007C01FC133F4848EB1F8049130F4848
EB07C04848EB03E0A2000F15F0491301001F15F8A2003F15FCA390C8FC4815FEA54815FF
B3A46C15FEA56D1301003F15FCA3001F15F8A26C6CEB03F0A36C6CEB07E0000315C06D13
0F6C6CEB1F806C6CEB3F00013E137C90381F81F8903807FFE0010090C7FC28447CC131>
48 D<143014F013011303131F13FFB5FC13E713071200B3B3B0497E497E007FB6FCA320
4278C131>I<ED0380A21507150FA2151F153FA2157F15FFA25CEC03BF153F1407140614
0C141C141814301470146014C013011480EB03005B13065B131C13185B1370136013E048
5A5B120390C7FC1206120E120C5A123812305A12E0B812C0A3C8383F8000ADEDFFE0027F
EBFFC0A32A437DC231>52 D E
%EndDVIPSBitmapFont
/Fc 64[50 29[39 12[55 55 25[44 44 66 44 50 28 39 39 1[50
50 50 72 28 44 1[28 50 50 28 44 50 44 50 50 10[61 2[50
4[66 83 55 2[33 2[61 1[72 66 61 61 15[50 2[25 33 25 2[33
33 37[50 2[{TeXBase1Encoding ReEncodeFont}45 99.6264
/Times-Italic rf
%DVIPSBitmapFont: Fd cmmi12 12 3
/Fd 3 103 df<F001C0F007E0181FF07FC0943801FF00EF07FCEF1FF0EF7FC04C48C7FC
EE0FFCEE3FF0EEFFC0030390C8FCED0FF8ED3FE0EDFF80DA03FEC9FCEC1FF8EC7FE09038
01FF80D907FECAFCEB1FF0EB7FC04848CBFCEA07FCEA1FF0EA7FC048CCFCA2EA7FC0EA1F
F0EA07FCEA01FF38007FC0EB1FF0EB07FE903801FF809038007FE0EC1FF8EC03FE913800
FF80ED3FE0ED0FF8ED03FF030013C0EE3FF0EE0FFCEE01FF9338007FC0EF1FF0EF07FCEF
01FF9438007FC0F01FE01807F001C03B3878B44C>60 D<127012FCB4FCEA7FC0EA1FF0EA
07FCEA01FF38007FC0EB1FF0EB07FE903801FF809038007FE0EC1FF8EC03FE913800FF80
ED3FE0ED0FF8ED03FF030013C0EE3FF0EE0FFCEE01FF9338007FC0EF1FF0EF07FCEF01FF
9438007FC0F01FE0A2F07FC0943801FF00EF07FCEF1FF0EF7FC04C48C7FCEE0FFCEE3FF0
EEFFC0030390C8FCED0FF8ED3FE0EDFF80DA03FEC9FCEC1FF8EC7FE0903801FF80D907FE
CAFCEB1FF0EB7FC04848CBFCEA07FCEA1FF0EA7FC048CCFC12FC12703B3878B44C>62
D<EE07E0EE1FF8EE7C1CEEF80E923801F03E923803E07F17FFED07E116C117FE92380FC0
FC177817004B5AA4153F93C7FCA45D157EA491B61280A3DA00FCC7FCA314015DA414035D
A414075DA4140F5DA5141F5DA4143F92C8FCA45C147EA45CA45C1301A25CA2EA1C03007F
5B12FF5C13075C4848C9FC12F8EA601EEA783CEA1FF0EA07C0305A7BC530>102
D E
%EndDVIPSBitmapFont
/Fe 134[42 2[42 42 23 32 28 1[42 42 42 65 23 2[23 42
42 28 37 42 1[42 37 12[51 10[28 4[60 1[55 19[21 28 21
44[{TeXBase1Encoding ReEncodeFont}26 83.022 /Times-Roman
rf
%DVIPSBitmapFont: Ff cmr7 7 2
/Ff 2 51 df<13381378EA01F8121F12FE12E01200B3AB487EB512F8A215267BA521>49
D<13FF000313E0380E03F0381800F848137C48137E00787F12FC6CEB1F80A4127CC7FC15
005C143E147E147C5C495A495A5C495A010EC7FC5B5B903870018013E0EA018039030003
0012065A001FB5FC5A485BB5FCA219267DA521>I E
%EndDVIPSBitmapFont
/Fg 103[60 26[60 1[60 60 60 60 60 60 60 60 60 60 60 60
60 60 60 60 2[60 60 60 60 60 60 60 60 60 3[60 1[60 3[60
60 1[60 60 1[60 60 1[60 60 3[60 1[60 1[60 60 60 1[60
60 1[60 1[60 1[60 60 60 60 60 60 60 60 60 60 60 60 60
60 60 5[60 38[{TeXBase1Encoding ReEncodeFont}62 99.6264
/Courier rf
%DVIPSBitmapFont: Fh cmr8 8 2
/Fh 2 51 df<130C133C137CEA03FC12FFEAFC7C1200B3B113FE387FFFFEA2172C7AAB23
>49 D<EB7F803801FFF0380780FC380E003F48EB1F8048EB0FC05A0060EB07E012F000FC
14F07E1403A3007C1307C7FCA215E0140F15C0141F1580EC3F00147E147C5C495A495A49
5A495A011EC7FC5B5B4913305B485A4848136048C7FC000E14E0001FB5FC5A4814C0B6FC
A21C2C7DAB23>I E
%EndDVIPSBitmapFont
/Fi 105[50 28[50 50 2[55 33 39 44 1[55 50 55 83 28 2[28
1[50 33 44 55 44 55 50 10[72 1[66 55 3[78 72 94 66 3[78
1[61 66 72 72 66 72 13[50 50 50 1[28 25 33 45[{
TeXBase1Encoding ReEncodeFont}40 99.6264 /Times-Bold
rf /Fj 139[40 1[53 1[66 60 66 100 33 2[33 3[53 3[60 23[47
2[73 18[60 60 60 2[30 46[{TeXBase1Encoding ReEncodeFont}16
119.552 /Times-Bold rf
%DVIPSBitmapFont: Fk cmsy10 12 1
/Fk 1 16 df<49B4FC010F13E0013F13F8497F48B6FC4815804815C04815E04815F0A248
15F8A24815FCA3B712FEA96C15FCA36C15F8A26C15F0A26C15E06C15C06C15806C15006C
6C13FC6D5B010F13E0010190C7FC27277BAB32>15 D E
%EndDVIPSBitmapFont
/Fl 64[44 42[44 44 24[44 50 50 72 50 50 28 39 33 50 50
50 50 78 28 50 28 28 50 50 33 44 50 44 50 44 6[61 1[72
94 72 72 61 55 66 72 55 72 72 89 61 1[39 33 72 72 55
61 72 66 66 72 3[56 1[28 28 50 50 50 50 50 50 50 50 50
50 28 25 33 25 2[33 33 36[55 55 2[{TeXBase1Encoding ReEncodeFont}74
99.6264 /Times-Roman rf
%DVIPSBitmapFont: Fm cmsy10 14.4 2
/Fm 2 104 df<EE1FE0ED01FF150F92383FF800EDFFC04A90C7FC4A5A4A5A4A5A4A5A5D
A2143F5DB3B1147F5D14FF92C8FC5B495A495A495AEB3FE0EBFF80D87FFEC9FCEAFFF8A2
EA7FFEC66C7EEB3FE0EB0FF86D7E6D7E6D7E7F81147F81143FB3B181141FA2816E7E6E7E
6E7E6E7E6E13C0ED3FF892380FFFE01501ED001F2B7878D93C>102
D<B4FC13F813FF000313C038007FF0EB1FF8EB07FC6D7E6D7E6D7F147FA281143FB3B181
141F81140F816E7E6E7E6E7E6E6C7EED3FF092380FFFC0030113E0A2030F13C092383FF0
00ED7F804A48C7FC4A5A4A5A4A5A5D141F5D143F5DB3B1147F5DA214FF4990C8FC495A49
5AEB1FF8EB7FF03803FFC0B5C9FC13F890CAFC2B7878D93C>I E
%EndDVIPSBitmapFont
/Fn 105[60 27[53 4[60 33 47 40 60 60 60 60 93 33 2[33
1[60 40 53 60 53 60 53 7[86 4[73 66 1[86 66 3[73 2[40
1[86 1[73 86 80 1[86 110 5[33 60 4[60 1[60 60 60 1[30
40 30 44[{TeXBase1Encoding ReEncodeFont}42 119.552 /Times-Roman
rf /Fo 136[104 1[80 48 56 64 1[80 72 80 120 40 80 1[40
1[72 1[64 80 64 80 72 12[96 80 104 1[88 1[104 135 3[56
2[88 1[104 104 96 104 6[48 1[72 72 72 72 72 72 72 72
72 1[36 46[{TeXBase1Encoding ReEncodeFont}41 143.462
/Times-Bold rf end
%%EndProlog
%%BeginSetup
%%Feature: *Resolution 600dpi
TeXDict begin
%%BeginPaperSize: Letter
letter
%%EndPaperSize

%%EndSetup
%%Page: 1 1
1 0 bop 472 600 a Fo(DDDMP:)35 b(Decision)f(Diagram)f(DuMP)j(package)
1480 830 y(Release)e(2.0)462 1230 y Fn(Gianpiero)c(Cabodi)2402
1232 y(Stef)o(ano)g(Quer)1316 1506 y(Politecnico)g(di)g(T)-10
b(orino)1024 1656 y(Dip.)30 b(di)g(Automatica)g(e)g(Informatica)1119
1805 y(Corso)f(Duca)h(de)n(gli)g(Abruzzi)g(24)1277 1955
y(I\22610129)e(T)-5 b(urin,)29 b(IT)-11 b(AL)f(Y)1038
2104 y(E-mail:)38 b Fm(f)p Fn(cabodi,quer)p Fm(g)p Fn(@polito.it)-189
2614 y Fo(1)143 b(Intr)m(oduction)-189 2837 y Fl(The)27
b(DDDMP)h(package)f(de\002nes)h(formats)f(and)g(rules)g(to)g(store)g
(DD)g(on)g(\002le.)39 b(More)27 b(in)g(particular)g(it)g(contains)g(a)
-189 2958 y(set)e(of)g(functions)e(to)i(dump)e(\(store)i(and)g(load\))g
(DDs)f(and)h(DD)g(forests)f(on)h(\002le)g(in)f(dif)n(ferent)h(formats.)
47 3078 y(In)30 b(the)g(present)g(implementation,)f(BDDs)h(\(R)l
(OBDDs\))h(and)f(ADD)g(\(Algebraic)g(Decision)g(Diagram\))g(of)-189
3199 y(the)g(CUDD)g(package)g(\(v)o(ersion)f(2.3.0)g(or)h(higher\))g
(are)g(supported.)45 b(These)30 b(structures)f(can)h(be)g(represented)g
(on)-189 3319 y(\002les)25 b(either)g(in)f(te)o(xt,)g(binary)-6
b(,)24 b(or)h(CNF)g(\(DIMA)l(CS\))h(formats.)47 3439
y(The)f(main)f(rules)h(used)f(are)i(follo)n(wing)d(rules:)-44
3643 y Fk(\017)49 b Fl(A)30 b(\002le)h(contains)e(a)i(single)e(BDD/ADD)
h(or)g(a)h(forest)f(of)g(BDDs/ADD,)g(i.e.,)i(a)e(v)o(ector)g(of)g
(Boolean)h(func-)55 3763 y(tions.)-44 3966 y Fk(\017)49
b Fl(Inte)o(ger)21 b(inde)o(x)o(es)f(are)i(used)f(instead)g(of)g
(pointers)g(to)g(reference)i(nodes.)29 b(BDD/ADD)21 b(nodes)g(are)h
(numbered)55 4087 y(with)j(contiguous)g(numbers,)g(from)h(1)g(to)f
(NNodes)h(\(total)f(number)h(of)g(nodes)g(on)f(a)i(\002le\).)35
b(0)26 b(is)f(not)h(used)f(to)55 4207 y(allo)n(w)f(ne)o(gati)n(v)o(e)e
(inde)o(x)o(es)h(for)i(complemented)f(edges.)-44 4411
y Fk(\017)49 b Fl(A)23 b(\002le)g(contains)f(a)h(header)l(,)h
(including)d(se)n(v)o(eral)h(informations)f(about)h(v)n(ariables)h(and)
f(roots)g(of)h(BDD)h(func-)55 4531 y(tions,)32 b(then)e(the)h(list)g
(of)g(nodes.)49 b(The)32 b(header)f(is)g(al)o(w)o(ays)g(represented)h
(in)f(te)o(xt)f(format)h(\(also)g(for)g(binary)55 4651
y(\002les\).)g(BDDs,)25 b(ADDs,)f(and)h(CNF)h(\002les)f(share)g(a)g
(similar)f(format)g(header)-5 b(.)-44 4855 y Fk(\017)49
b Fl(BDD/ADD)40 b(nodes)g(are)h(listed)f(follo)n(wing)e(their)i
(numbering,)j(which)d(is)g(produced)g(by)h(a)f(post-order)55
4975 y(tra)n(v)o(ersal,)24 b(in)h(such)f(a)h(w)o(ay)g(that)g(a)g(node)f
(is)h(al)o(w)o(ays)f(listed)g(after)h(its)f(Then/Else)g(children.)47
5179 y(In)32 b(the)f(sequel)g(we)g(describe)h(more)f(in)g(detail)f(the)
h(dif)n(ferent)g(formats)g(and)g(procedures)h(a)n(v)n(ailable.)49
b(First)-189 5299 y(of)26 b(all,)f(we)h(describe)f(BDDs)h(and)g(ADDs)f
(formats)g(and)g(procedure.)33 b(Secondly)-6 b(,)26 b(we)f(concentrate)
h(on)f(CNF)i(\002les,)-189 5419 y(i.e.,)e(ho)n(w)f(to)g(translate)g(a)i
(BDD)f(or)g(a)g(forest)g(of)f(BDDs)h(into)f(a)h(CNF)h(formula)e(and)h
(vice-v)o(ersa.)1794 5800 y(1)p eop
%%Page: 2 2
2 1 bop -189 218 a Fo(2)143 b(BDD)35 b(and)g(ADD)g(Support)-189
441 y Fl(In)23 b(this)f(section)g(we)g(describe)h(format)g(and)f
(procedure)h(re)o(garding)f(BDDs)h(and)f(ADDs.)30 b(W)-8
b(e)23 b(speci\002cally)g(refer)g(to)-189 562 y(BDDs)h(in)g(the)g
(description)e(as)j(ADD)e(may)h(be)g(seen)g(as)h(an)f(e)o(xtension)e
(and)i(will)f(be)h(described)g(later)-5 b(.)30 b(First)24
b(of)g(all,)-189 682 y(we)29 b(concentrate)f(on)g(the)g(format)g(used)g
(to)g(store)g(these)g(structure,)h(then)f(we)g(describe)h(the)f
(procedure)h(a)n(v)n(ailable)-189 802 y(to)24 b(store)h(and)g(load)f
(them.)-189 1094 y Fj(2.1)119 b(F)m(ormat)-189 1281 y
Fl(BDD)30 b(dump)f(\002les)g(are)i(composed)e(of)g(tw)o(o)g(sections:)
40 b(The)29 b(header)h(and)g(the)f(list)g(of)h(nodes.)44
b(The)30 b(header)g(has)g(a)-189 1402 y(common)c(\(te)o(xt\))h(format,)
h(while)e(the)i(list)e(of)h(nodes)g(is)g(either)g(in)g(te)o(xt)g(or)g
(binary)g(format.)38 b(In)28 b(te)o(xt)e(format)h(nodes)-189
1522 y(are)33 b(represented)f(with)f(redundant)g(informations,)h(where)
h(the)f(main)f(goal)g(is)h(readability)-6 b(,)32 b(while)g(the)f
(purpose)-189 1642 y(of)i(binary)f(format)g(is)g(minimizing)e(the)i(o)o
(v)o(erall)f(storage)h(size)h(for)g(BDD)f(nodes.)54 b(The)32
b(header)h(format)f(is)g(k)o(ept)-189 1763 y(common)h(to)h(te)o(xt)g
(and)g(binary)g(formats)g(for)h(sak)o(e)f(of)h(simplicity:)47
b(No)34 b(particular)g(optimization)f(is)h(presently)-189
1883 y(done)29 b(on)f(binary)h(\002le)g(headers,)h(whose)f(size)g(is)f
(by)h(f)o(ar)g(dominated)f(by)h(node)f(lists)g(in)g(the)h(case)g(of)g
(lar)n(ge)h(BDDs)-189 2003 y(\(se)n(v)o(eral)24 b(thousands)g(of)h(DD)f
(nodes\).)-189 2266 y Fi(2.1.1)99 b(Header)-189 2453
y Fl(The)23 b(header)h(has)f(the)g(same)g(format)g(both)g(for)g(te)o
(xtual)f(and)i(binary)e(dump.)30 b(F)o(or)23 b(sak)o(e)g(of)h
(generality)e(and)h(because)-189 2574 y(of)f(dynamic)g(v)n(ariable)g
(ordering)g(both)f(v)n(ariable)h(IDs)g(and)g(permutations)2377
2537 y Fh(1)2438 2574 y Fl(are)h(included.)29 b(Names)22
b(are)h(optionally)-189 2694 y(listed)35 b(for)h(input)f(v)n(ariables)g
(and)h(for)h(the)e(stored)h(functions.)63 b(Ne)n(w)36
b(auxiliary)f(IDs)h(are)h(also)e(allo)n(wed.)64 b(Only)-189
2814 y(the)34 b(v)n(ariables)f(in)g(the)h(true)g(support)f(of)h(the)f
(stored)h(BDDs)g(are)h(listed.)56 b(All)34 b(information)e(on)i(v)n
(ariables)f(\(IDs,)-189 2935 y(permutations,)c(names,)i(auxiliary)e
(IDs\))h(sorted)g(by)g(IDs,)h(and)e(the)o(y)h(are)g(restricted)g(to)f
(the)h(true)g(support)f(of)h(the)-189 3055 y(dumped)22
b(BDD,)h(while)g(IDs)g(and)f(permutations)g(are)h(referred)i(to)d(the)h
(writing)f(BDD)h(manager)-5 b(.)30 b(Names)22 b(can)i(thus)-189
3175 y(be)h(sorted)f(by)h(v)n(ariable)f(ordering)h(by)f(permuting)g
(them)g(according)h(to)f(the)h(permutations)e(stored)h(in)h(the)f
(\002le.)47 3296 y(As)h(an)g(e)o(xample,)f(the)g(header)i(\(in)e(te)o
(xt)g(mode\))h(of)f(the)h(ne)o(xt)f(state)h(functions)e(of)i(circuit)g
(s27)f(follo)n(ws:)-189 3494 y Fg(.ver)59 b(DDDMP-2.0)-189
3615 y(.mode)g(A)-189 3735 y(.varinfo)f(3)-189 3855 y(.dd)h(s27-delta)
-189 3976 y(.nnodes)f(16)-189 4096 y(.nvars)g(10)-189
4216 y(.nsuppvars)g(7)-189 4337 y(.varnames)g(G0)h(G1)g(G2)h(G3)f(G5)g
(G6)h(G7)-189 4457 y(.orderedvarnames)c(G0)k(G1)f(G2)g(G3)h(G5)f(G6)g
(G7)-189 4578 y(.ids)g(0)g(1)h(2)g(3)f(4)h(5)f(6)-189
4698 y(.permids)f(0)i(1)f(2)h(3)f(5)h(7)f(9)-189 4818
y(.auxids)f(1)i(2)f(3)h(4)f(5)h(6)g(7)-189 4939 y(.nroots)e(3)-189
5059 y(.rootids)g(6)i(-13)f(-16)-189 5179 y(.rootnames)f(G10)h(G11)g
(G13)47 5378 y Fl(The)25 b(lines)f(contain)g(the)h(follo)n(wing)e
(informations:)p -189 5460 1607 4 v -77 5521 a Ff(1)-40
5551 y Fe(The)d(permutation)e(of)i(the)g(i-th)h(v)n(ariable)e(ID)h(is)h
(the)f(relati)n(v)o(e)g(position)f(of)h(the)g(v)n(ariable)f(in)i(the)f
(ordering.)1794 5800 y Fl(2)p eop
%%Page: 3 3
3 2 bop -44 218 a Fk(\017)49 b Fl(Dddmp)24 b(v)o(ersion)f(information.)
-44 411 y Fk(\017)49 b Fl(File)25 b(mode)f(\(A)h(for)g(ASCII)h(te)o
(xt,)e(B)h(for)g(binary)g(mode\).)-44 604 y Fk(\017)49
b Fl(V)-11 b(ar)n(-e)o(xtra-info)25 b(\(0:)30 b(v)n(ariable)24
b(ID,)h(1:)31 b(permID,)24 b(2:)31 b(aux)25 b(ID,)g(3:)30
b(v)n(ariable)24 b(name,)h(4)g(no)f(e)o(xtra)h(info\).)-44
797 y Fk(\017)49 b Fl(Name)25 b(of)g(dd)f(\(optional\).)-44
990 y Fk(\017)49 b Fl(T)-8 b(otal)24 b(number)g(of)h(nodes)g(in)f(the)h
(\002le.)-44 1183 y Fk(\017)49 b Fl(Number)24 b(of)h(v)n(ariables)f(of)
h(the)g(writing)f(DD)g(manager)-5 b(.)-44 1375 y Fk(\017)49
b Fl(Number)24 b(of)h(v)n(ariables)f(in)h(the)f(true)h(support)f(of)h
(the)f(stored)h(DDs.)-44 1568 y Fk(\017)49 b Fl(V)-11
b(ariable)25 b(names)f(\(optional\))g(for)h(all)g(the)f(v)n(ariables)g
(in)h(the)f(BDD/ADD)h(support.)-44 1761 y Fk(\017)49
b Fl(V)-11 b(ariable)20 b(names)g(for)h(all)f(the)g(v)n(ariables)f(in)h
(the)g(DD)h(manager)f(during)g(the)g(storing)f(phase.)29
b(Notice)20 b(that)g(this)55 1882 y(information)k(w)o(as)h(not)g
(stored)g(by)g(pre)n(vious)f(v)o(ersions)g(of)i(the)f(same)g(tool.)32
b(Full)25 b(backw)o(ard)g(compatibility)55 2002 y(is)f(guaranteed)h(by)
g(the)f(present)h(implementation)d(of)j(the)g(tool.)-44
2195 y Fk(\017)49 b Fl(V)-11 b(ariable)25 b(IDs.)-44
2388 y Fk(\017)49 b Fl(V)-11 b(ariable)25 b(permuted)f(IDs.)-44
2581 y Fk(\017)49 b Fl(V)-11 b(ariable)25 b(auxiliary)f(IDs)h
(\(optional\).)-44 2774 y Fk(\017)49 b Fl(Number)24 b(of)h(BDD)g
(roots.)-44 2967 y Fk(\017)49 b Fl(Inde)o(x)o(es)24 b(of)h(BDD)g(roots)
f(\(complemented)g(edges)g(allo)n(wed\).)-44 3160 y Fk(\017)49
b Fl(Names)24 b(of)h(BDD)h(roots)e(\(optional\).)-189
3332 y(Notice)h(that)f(a)h(\002eld)-189 3504 y Fg(.add)-189
3676 y Fl(is)f(present)h(after)g(the)g(dddmp)f(v)o(ersion)f(for)j
(\002les)e(containing)g(ADDs.)-189 3936 y Fi(2.1.2)99
b(T)-9 b(ext)25 b(F)n(ormat)-189 4124 y Fl(In)g(te)o(xt)f(mode)g(nodes)
g(are)i(listed)e(on)g(a)h(te)o(xt)f(line)h(basis.)30
b(Each)25 b(a)g(node)f(is)h(represented)g(as)-189 4296
y Fg(<Node-index>)57 b([<Var-extra-info>])f(<Var-internal-index>)588
4416 y(<Then-index>)h(<Else-index>)-189 4588 y Fl(where)25
b(all)g(inde)o(x)o(es)e(are)j(inte)o(ger)e(numbers.)47
4709 y(This)h(format)g(is)g(redundant)f(\(due)i(to)f(the)g(node)g
(ordering,)g Fd(<)p Fl(Node-inde)o(x)p Fd(>)f Fl(is)g(and)i
(incremental)e(inte)o(ger\))-189 4829 y(b)n(ut)g(we)h(k)o(eep)g(it)g
(for)g(readability)-6 b(.)47 4949 y Fd(<)p Fl(V)-11 b(ar)n(-e)o
(xtra-info)p Fd(>)34 b Fl(\(optional)e(redundant)i(\002eld\))g(is)f
(either)h(an)g(inte)o(ger)f(\(ID,)h(PermID,)g(or)g(auxID\))g(or)g(a)
-189 5070 y(string)k(\(v)n(ariable)h(name\).)75 b Fd(<)p
Fl(V)-11 b(ar)n(-internal-inde)o(x)p Fd(>)38 b Fl(is)h(an)g(internal)g
(v)n(ariable)g(inde)o(x:)59 b(V)-11 b(ariables)39 b(in)g(the)g(true)
-189 5190 y(support)25 b(of)h(the)g(stored)g(BDDs)g(are)h(numbered)e
(with)g(ascending)h(inte)o(gers)f(starting)g(from)h(0,)g(and)g(follo)n
(wing)e(the)-189 5311 y(v)n(ariable)g(ordering.)31 b
Fd(<)p Fl(Then-inde)o(x)p Fd(>)23 b Fl(and)i Fd(<)p Fl(Else-inde)o(x)p
Fd(>)e Fl(are)j(signed)e(inde)o(x)o(es)f(of)i(children)f(nodes.)47
5431 y(In)h(the)f(follo)n(wing,)f(we)i(report)f(the)g(list)g(of)h
(nodes)f(of)g(the)h(s27)f(ne)o(xt)f(state)i(functions)e(\(see)i(pre)n
(vious)e(header)-189 5551 y(e)o(xample\):)1794 5800 y(3)p
eop
%%Page: 4 4
4 3 bop -189 218 a Fg(.nodes)-189 338 y(1)60 b(T)f(1)h(0)f(0)-189
459 y(2)h(G7)f(6)g(1)h(-1)-189 579 y(3)g(G5)f(4)g(1)h(2)-189
699 y(4)g(G3)f(3)g(3)h(1)-189 820 y(5)g(G1)f(1)g(1)h(4)-189
940 y(6)g(G0)f(0)g(5)h(-1)-189 1061 y(7)g(G6)f(5)g(1)h(-1)-189
1181 y(8)g(G5)f(4)g(1)h(-7)-189 1301 y(9)g(G6)f(5)g(1)h(-2)-189
1422 y(10)f(G5)h(4)f(1)h(-9)-189 1542 y(11)f(G3)h(3)f(10)h(8)-189
1662 y(12)f(G1)h(1)f(8)h(11)-189 1783 y(13)f(G0)h(0)f(5)h(12)-189
1903 y(14)f(G2)h(2)f(1)h(-1)-189 2024 y(15)f(G2)h(2)f(1)h(-2)-189
2144 y(16)f(G1)h(1)f(14)h(15)-189 2264 y(.end)-189 2468
y Fl(The)27 b(list)f(is)h(enclosed)g(between)g(the)g
Fg(.nodes)f Fl(and)h Fg(.end)f Fl(lines.)37 b(First)27
b(node)g(is)g(the)g(one)g(constant,)f(each)i(node)-189
2588 y(contains)c(the)h(optional)e(v)n(ariable)h(name.)47
2708 y(F)o(or)29 b(ADDs)f(more)h(than)f(one)h(constant)e(is)i(stored)f
(in)g(the)g(\002le.)43 b(Each)29 b(constant)f(has)g(the)h(same)f
(format)h(we)-189 2829 y(ha)n(v)o(e)c(just)e(analyzed)i(for)g(the)g
(BDD)g(b)n(ut)g(the)f(represented)h(v)n(alue)f(is)h(stored)f(as)h(a)g
(\003oat)g(number)-5 b(.)-189 3095 y Fi(2.1.3)99 b(Binary)25
b(F)n(ormat)-189 3283 y Fl(The)h(binary)g(format)f(is)h(not)f(allo)n
(wed)g(for)i(ADDs.)33 b(As)26 b(a)h(consequence)f(we)g(concentrate)g
(only)f(on)h(BDDs)g(in)g(this)-189 3403 y(section.)k(In)25
b(binary)f(mode)h(nodes)f(are)i(represented)f(as)g(a)g(sequence)g(of)g
(bytes,)f(encoding)g(tuples)-189 3606 y Fg(<Node-code>)-189
3727 y([<Var-internal-info>])-189 3847 y([<Then-info>])-189
3968 y([<Else-info>])-189 4171 y Fl(in)30 b(an)g(optimized)f(w)o(ay)-6
b(.)46 b(Only)29 b(the)h(\002rst)g(byte)g(\(code\))h(is)e(mandatory)-6
b(,)30 b(while)g(inte)o(ger)f(inde)o(x)o(es)g(are)i(represented)-189
4291 y(in)c(absolute)f(or)h(relati)n(v)o(e)f(mode,)h(where)h(relati)n
(v)o(e)e(means)g(of)n(fset)h(with)f(respect)i(to)e(a)i(Then/Else)e
(node)h(info.)37 b(The)-189 4412 y(best)23 b(between)g(absolute)f(and)h
(relati)n(v)o(e)e(representation)i(is)f(chosen)h(and)g(relati)n(v)o(e)f
(1)h(is)f(directly)g(coded)h(in)g Fd(<)p Fl(Node-)-189
4532 y(code)p Fd(>)e Fl(without)f(an)o(y)g(e)o(xtra)h(info.)29
b(Suppose)21 b(V)-11 b(ar\(NodeId\),)22 b(Then\(NodeId\))f(and)g
(Else\(NodeId\))f(represent)i(infos)-189 4652 y(about)i(a)h(gi)n(v)o
(en)f(node.)30 b Fd(<)p Fl(Node-code)p Fd(>)25 b Fl(is)f(a)h(byte)g
(which)f(contains)g(the)h(follo)n(wing)e(bit)h(\002elds)h(\(MSB)g(to)g
(LSB\))-44 4856 y Fk(\017)49 b Fl(Unused)24 b(:)31 b(1)24
b(bit)-44 5059 y Fk(\017)49 b Fl(V)-11 b(ariable:)30
b(2)25 b(bits,)f(one)h(of)g(the)f(follo)n(wing)f(codes)171
5288 y Fi(\226)49 b Fl(DDDMP)p 636 5288 30 4 v 35 w(ABSOLUTE)p
1191 5288 V 36 w(ID:)22 b(V)-11 b(ar\(NodeId\))22 b(is)f(represented)h
(in)g(absolute)f(form)g(as)h Fd(<)p Fl(V)-11 b(ar)n(-internal-)270
5408 y(info)p Fd(>)24 b Fl(=)h(V)-11 b(ar\(NodeId\))25
b(follo)n(ws)e(\(absolute)i(info\))1794 5800 y(4)p eop
%%Page: 5 5
5 4 bop 171 218 a Fi(\226)49 b Fl(DDDMP)p 636 218 30
4 v 35 w(RELA)-11 b(TIVE)p 1147 218 V 36 w(ID:)32 b(V)-11
b(ar\(NodeId\))32 b(is)g(represented)g(in)f(relati)n(v)o(e)g(form)h(as)
g Fd(<)p Fl(V)-11 b(ar)n(-internal-)270 338 y(info\277)24
b(=)h(Min\(V)-11 b(ar\(Then\(NodeId\)\),V)g(ar\(Else\(NodeId\)\)\)-V)g
(ar\(NodeId\))171 500 y Fi(\226)49 b Fl(DDDMP)p 636 500
V 35 w(RELA)-11 b(TIVE)p 1147 500 V 36 w(1:)27 b(the)19
b(\002eld)g Fd(<)p Fl(V)-11 b(ar)n(-internal-info)p Fd(>)18
b Fl(does)h(not)f(follo)n(w)-6 b(,)18 b(because)h(V)-11
b(ar\(NodeId\))270 620 y(=)25 b(Min\(V)-11 b(ar\(Then\(NodeId\)\),V)g
(ar\(Else\(NodeId\)\)\)-1)171 782 y Fi(\226)49 b Fl(DDDMP)p
636 782 V 35 w(TERMIN)m(AL:)24 b(Node)h(is)f(a)h(terminal,)f(no)g(v)n
(ar)h(info)g(required)-44 1011 y Fk(\017)49 b Fl(T)25
b(:)f(2)h(bits,)f(with)g(codes)h(similar)e(to)i(V)171
1214 y Fi(\226)49 b Fl(DDDMP)p 636 1214 V 35 w(ABSOLUTE)p
1191 1214 V 36 w(ID:)20 b Fd(<)p Fl(Then-info)p Fd(>)f
Fl(is)h(represented)g(in)g(absolute)f(form)h(as)g Fd(<)p
Fl(Then-info)p Fd(>)270 1334 y Fl(=)25 b(Then\(NodeId\))171
1496 y Fi(\226)49 b Fl(DDDMP)p 636 1496 V 35 w(RELA)-11
b(TIVE)p 1147 1496 V 36 w(ID:)28 b(Then\(NodeId\))f(is)g(represented)h
(in)g(relati)n(v)o(e)e(form)i(as)g Fd(<)p Fl(Then-info)p
Fd(>)270 1617 y Fl(=)d(Nodeid-Then\(NodeId\))171 1779
y Fi(\226)49 b Fl(DDDMP)p 636 1779 V 35 w(RELA)-11 b(TIVE)p
1147 1779 V 36 w(1:)30 b(no)25 b Fd(<)p Fl(Then-info)p
Fd(>)f Fl(follo)n(ws,)f(because)i(Then\(NodeId\))g(=)g(NodeId-1)171
1941 y Fi(\226)49 b Fl(DDDMP)p 636 1941 V 35 w(TERMIN)m(AL:)24
b(Then)h(Node)f(is)h(a)g(terminal,)f(no)g(info)h(required)f(\(for)i(R)l
(OBDDs\))-44 2144 y Fk(\017)49 b Fl(Ecompl)24 b(:)30
b(1)25 b(bit,)f(if)h(1)g(means)f(that)g(the)h(else)g(edge)g(is)f
(complemented)-44 2347 y Fk(\017)49 b Fl(E)25 b(:)f(2)h(bits,)f(with)g
(codes)h(and)f(meanings)g(as)h(for)g(the)g(Then)f(edge)-189
2551 y(DD)35 b(node)f(codes)h(are)h(written)e(as)h(one)g(byte.)60
b Fd(<)p Fl(V)-11 b(ar)n(-internal-inde)o(x)p Fd(>)p
Fl(,)36 b Fd(<)p Fl(Then-inde)o(x)p Fd(>)p Fl(,)g Fd(<)p
Fl(Else-inde)o(x)p Fd(>)e Fl(\(if)-189 2671 y(required\))25
b(are)h(represented)f(as)g(unsigned)e(inte)o(ger)h(v)n(alues)g(on)h(a)g
(suf)n(\002cient)f(set)h(of)g(bytes)f(\(MSByte)h(\002rst\).)47
2792 y(Inte)o(gers)h(of)f(an)o(y)h(length)e(are)j(written)e(as)h
(sequences)g(of)g(\224link)o(ed\224)f(bytes)g(\(MSByte)h(\002rst\).)34
b(F)o(or)26 b(each)g(byte)-189 2912 y(7)f(bits)f(are)h(used)g(for)g
(data)g(and)f(one)h(\(MSBit\))g(as)g(link)f(with)g(a)h(further)g(byte)g
(\(MSB)g(=)g(1)g(means)f(one)h(more)g(byte\).)47 3032
y(Lo)n(w)f(le)n(v)o(el)g(read/write)h(of)g(bytes)f(\002lters)h
Fd(<)p Fl(CR)p Fd(>)p Fl(,)g Fd(<)p Fl(LF)p Fd(>)g Fl(and)g
Fd(<)p Fl(ctrl-Z)p Fd(>)f Fl(through)g(escape)h(sequences.)-189
3327 y Fj(2.2)119 b(Implementation)-189 3515 y Fl(Store)24
b(and)g(load)g(for)g(single)g(Boolean)g(functions)f(and)h(arrays)g(of)g
(Boolean)g(functions)f(are)i(implemented.)k(More-)-189
3635 y(o)o(v)o(er)l(,)37 b(the)e(current)h(presentation)f(includes)f
(functions)h(to)g(retrie)n(v)o(e)g(v)n(ariables)f(names,)k(auxiliary)d
(identi\002erss,)-189 3756 y(and)c(all)g(the)g(information)f(contained)
h(in)f(the)h(header)h(of)f(the)h(\002les.)50 b(This)30
b(information)g(can)h(be)h(used)f(as)g(a)g(pre-)-189
3876 y(processing)19 b(step)g(for)i(load)e(operations.)28
b(These)20 b(functions)f(allo)n(w)f(to)i(o)o(v)o(ercome)f(fe)n(w)g
(limitations)f(of)h(the)h(pre)n(vious)-189 3997 y(implementations.)-189
4263 y Fi(2.2.1)99 b(Storing)25 b(Decision)g(Diagrams)-189
4450 y Fc(Dddmp)p 111 4450 V 35 w(cuddBddStor)l(e)f Fl(and)h
Fc(Dddmp)p 1195 4450 V 35 w(cuddBddArr)o(ayStor)l(e)e
Fl(are)j(the)f(tw)o(o)f(store)h(functions,)f(used)h(to)g(store)f(sin-)
-189 4571 y(gle)f(BDD)h(or)g(a)f(forest)h(of)f(BDDs,)h(respecti)n(v)o
(ely)-6 b(.)28 b(Internally)-6 b(,)23 b Fc(Dddmp)p 2275
4571 V 35 w(cuddBddStor)l(e)f Fl(b)n(uilds)g(a)i(dummy)e(1)h(entry)-189
4691 y(array)j(of)e(BDDs,)h(and)g(calls)g Fc(dddmp)p
1102 4691 V 35 w(cuddBddArr)o(ayStor)l(e)p Fl(.)47 4811
y(Since)30 b(con)l(v)o(ersion)e(from)h(DD)h(pointers)e(to)h(inte)o(ger)
f(is)h(required,)i(DD)e(nodes)g(are)h(temporarily)e(remo)o(v)o(ed)-189
4932 y(from)23 b(the)f(unique)h(hash.)29 b(This)23 b(mak)o(es)f(room)g
(in)h(their)f Fc(ne)n(xt)h Fl(\002eld)h(to)e(store)h(node)f(IDs.)30
b(Nodes)23 b(are)h(re-link)o(ed)e(after)-189 5052 y(the)i(store)g
(operation,)g(possible)f(in)g(a)i(modi\002ed)e(order)-5
b(.)31 b(Dumping)22 b(is)i(either)g(in)g(te)o(xt)f(or)i(binary)f(form.)
30 b(Both)24 b(a)g(\002le)-189 5173 y(pointer)31 b(\()p
Fc(fp)p Fl(\))g(and)g(a)h(\002le)g(name)f(\()p Fc(fname)p
Fl(\))h(are)g(pro)o(vided)e(as)h(inputs)f(parameters)i(to)f(store)g
(routines.)50 b(BDDs)31 b(are)-189 5293 y(stored)c(to)g(the)g(already)g
(open)h(\002le)f Fc(fp)p Fl(,)h(if)f(not)g(NULL.)g(Otherwise)f(\002le)i
(whose)f(name)g(is)g Fc(fname)g Fl(is)g(opened.)38 b(This)-189
5413 y(is)24 b(intended)g(to)h(allo)n(w)f(either)g(DD)h(storage)g
(within)e(\002les)i(containing)f(other)g(data,)h(or)g(to)g(speci\002c)g
(\002les.)1794 5800 y(5)p eop
%%Page: 6 6
6 5 bop -189 218 a Fi(2.2.2)99 b(Loading)25 b(Decision)g(Diagrams)-189
405 y Fc(Dddmp)p 111 405 30 4 v 35 w(cuddBddLoad)37 b
Fl(and)h Fc(Dddmp)p 1219 405 V 35 w(cuddBddArr)o(ayLoad)f
Fl(are)h(the)g(load)g(functions,)i(which)e(read)g(a)g(BDD)-189
526 y(dump)24 b(\002le.)47 646 y(F)o(ollo)n(wing)34 b(the)h(store)h
(function,)h(the)f(main)f(BDD)h(load)f(function,)j Fc(Dddmp)p
2813 646 V 35 w(cuddBddLoad)p Fl(,)f(is)f(imple-)-189
767 y(mented)g(by)g(calling)f(the)h(main)g(BDD-array)h(loading)f
(function)f Fc(Dddmp)p 2466 767 V 35 w(cuddBddArr)o(ayLoad)p
Fl(.)63 b(A)37 b(dynamic)-189 887 y(v)o(ector)24 b(of)h(DD)g(pointers)f
(is)g(temporarily)g(allocated)h(to)f(support)g(con)l(v)o(ersion)f(from)
i(DD)g(inde)o(x)o(es)e(to)h(pointers.)47 1007 y(Se)n(v)o(eral)40
b(criteria)f(are)i(supported)d(for)i(v)n(ariable)f(match)g(between)g
(\002le)h(and)g(DD)f(manager)l(,)k(practically)-189 1128
y(allo)n(wing)37 b(v)n(ariable)h(permutations)f(or)i(compositions)d
(while)i(loading)g(DDs.)71 b(V)-11 b(ariable)39 b(match)f(between)h
(the)-189 1248 y(DD)32 b(manager)g(and)g(the)g(BDD)g(\002le)g(is)g
(optionally)e(based)i(in)f Fc(IDs)p Fl(,)j Fc(perids)p
Fl(,)f Fc(varnames)p Fl(,)g Fc(var)o(auxids)p Fl(;)g(also)f(direct)-189
1369 y(composition)j(between)j Fc(IDs)g Fl(and)f Fc(composeids)g
Fl(is)g(supported.)68 b(The)38 b Fc(varmatc)o(hmode)e
Fl(parameter)i(is)f(used)g(to)-189 1489 y(select)27 b(mathing)e(mode.)
37 b(More)27 b(in)f(detail,)h(tw)o(o)f(match)h(modes)f(use)h(the)f
(information)g(within)f(the)i(DD)g(manager)l(,)-189 1609
y(the)e(other)f(ones)h(use)g(e)o(xtra)f(information,)f(which)i(support)
f(an)o(y)g(v)n(ariable)g(remap)h(or)g(change)g(in)f(the)h(ordering.)-44
1813 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p 1040 1813
V 35 w(V)-13 b(AR)p 1272 1813 V 35 w(MA)i(TCHIDS)19 b(allo)n(ws)f
(loading)g(a)h(DD)g(k)o(eeping)f(v)n(ariable)g(IDs)h(unchanged)55
1933 y(\(re)o(gardless)24 b(of)h(the)f(v)n(ariable)h(ordering)f(of)h
(the)g(reading)f(manager)-5 b(.)55 2095 y(This)24 b(is)g(useful,)g(for)
h(e)o(xample,)f(when)g(sw)o(apping)g(DDs)g(to)h(\002le)g(and)f
(restoring)g(them)g(later)h(from)f(\002le,)h(after)55
2215 y(possible)e(v)n(ariable)i(reordering)g(acti)n(v)n(ations.)-44
2419 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p 1040 2419
V 35 w(V)-13 b(AR)p 1272 2419 V 35 w(MA)i(TCHPERMIDS)36
b(is)e(used)h(to)f(allo)n(w)g(v)n(ariable)g(match)h(according)55
2539 y(to)h(the)h(position)e(in)i(the)g(ordering)f(\(retrie)n(v)o(ed)g
(by)h(array)h(of)f(permutations)e(stored)h(on)h(\002le)g(and)g(within)
55 2660 y(the)h(reading)g(DD)h(manager\).)72 b(A)38 b(possible)f
(application)h(is)g(retrie)n(ving)f(BDDs)i(stored)f(after)h(dynamic)55
2780 y(reordering,)28 b(from)g(a)g(DD)g(manager)g(where)h(all)e(v)n
(ariable)h(IDs)f(map)h(their)f(position)g(in)g(the)h(ordering,)g(and)55
2900 y(the)d(loaded)f(BDD)h(k)o(eeps)g(the)g(ordering)f(as)h(stored)f
(on)h(\002le.)-44 3104 y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p
1040 3104 V 35 w(V)-13 b(AR)p 1272 3104 V 35 w(MA)i(TCHN)m(AMES)26
b(requires)h(a)h(not)e(NULL)h(v)n(armatchmodes)f(param-)55
3224 y(eter;)34 b(this)c(is)g(a)h(v)o(ector)g(of)g(strings)e(in)i
(one-to-one)f(correspondence)h(with)f(v)n(ariable)h(IDs)f(of)h(the)g
(reading)55 3344 y(manager)-5 b(.)40 b(V)-11 b(ariables)28
b(in)g(the)g(DD)g(\002le)g(read)h(are)g(matched)f(with)f(manager)h(v)n
(ariables)f(according)h(to)g(their)55 3465 y(name)35
b(\(a)h(not)f(NULL)g(v)n(arnames)g(parameter)h(w)o(as)f(required)h
(while)f(storing)f(the)h(DD)g(\002le\).)64 b(The)35 b(most)55
3585 y(common)c(usage)h(of)g(this)f(feature)i(is)e(in)h(combination)e
(with)i(a)g(v)n(ariable)g(ordering)g(stored)f(on)h(a)g(\002le)h(and)55
3706 y(based)28 b(on)h(v)n(ariables)f(names.)41 b(Names)29
b(must)e(be)i(loaded)f(in)g(an)h(array)g(of)g(strings)e(and)i(passed)f
(to)g(the)h(DD)55 3826 y(load)24 b(procedure.)-44 4029
y Fk(\017)49 b Fl(v)n(armatchnode=DDDMP)p 1040 4029 V
35 w(V)-13 b(AR)p 1272 4029 V 35 w(MA)i(TCHIDS)25 b(has)g(a)g(meaning)f
(similar)g(to)55 4150 y(DDDMP)p 421 4150 V 36 w(V)-13
b(AR)p 654 4150 V 35 w(MA)i(TCHN)m(AMES)26 b(b)n(ut)h(inte)o(ger)f
(auxiliary)g(IDs)h(are)h(used)f(instead)f(of)h(strings.)36
b(The)28 b(ad-)55 4270 y(ditional)23 b(not)h(NULL)h(v)n(armathauxids)e
(parameter)i(is)g(needed.)-44 4474 y Fk(\017)49 b Fl(v)n
(armatchnode=DDDMP)p 1040 4474 V 35 w(V)-13 b(AR)p 1272
4474 V 35 w(COMPOSEIDS,)38 b(uses)f(the)f(additional)f(v)n
(arcomposeids)g(parameter)55 4594 y(as)25 b(an)g(array)g(of)g(v)n
(ariable)f(IDs)h(to)g(be)g(composed)f(with)g(IDs)g(stored)h(in)f
(\002le.)-189 4860 y Fi(2.2.3)99 b(DD)25 b(Load/Stor)n(e)h(and)f(V)-9
b(ariable)25 b(Ordering)-189 5048 y Fl(Loading)31 b(of)i(Decision)e
(Diagrams)h(from)g(\002le)g(supports)f(dif)n(ferent)h(v)n(ariables)g
(ordering)f(strate)o(gies,)i(as)g(already)-189 5168 y(pointed)23
b(out)h(in)g(the)h(pre)n(vious)e(section.)30 b(This)24
b(allo)n(ws)f(or)h(e)o(xample)g(storing)f(dif)n(ferent)i(BDDs)f(each)h
(with)f(its)g(o)n(wn)-189 5288 y(v)n(ariable)29 b(ordering,)h(and)g(to)
f(mer)n(ge)h(them)f(within)f(the)i(same)f(DD)h(manager)f(by)h(means)f
(of)g(proper)h(load)f(opera-)-189 5409 y(tions.)44 b(W)-8
b(e)30 b(suggest)f(using)f(DDDMP)p 1175 5409 V 36 w(V)-13
b(AR)p 1408 5409 V 36 w(MA)i(TCHIDS)30 b(whene)n(v)o(er)f(IDs)g(k)o
(eeps)h(on)f(representing)h(the)f(same)-189 5529 y(entities)24
b(while)h(changing)f(v)n(ariable)h(ordering.)31 b(If)25
b(this)f(is)h(not)f(true,)h(v)n(ariable)g(names)g(\(if)g(a)n(v)n
(ailable\))f(or)i(auxiliary)1794 5800 y(6)p eop
%%Page: 7 7
7 6 bop -189 218 a Fl(IDs)34 b(are)h(a)g(good)e(w)o(ay)i(to)f
(represent)g(in)l(v)n(ariant)f(attrib)n(uted)g(of)i(v)n(ariables)e
(across)h(se)n(v)o(eral)g(runs)g(with)f(dif)n(ferent)-189
338 y(orderings.)50 b(DDDMP)p 629 338 30 4 v 35 w(V)-13
b(AR)p 861 338 V 36 w(COMPOSEIDS)32 b(is)f(an)h(alternati)n(v)o(e)e
(solution,)h(that)g(practically)f(corresponds)h(to)-189
459 y(cascading)23 b(DDDMP)p 593 459 V 36 w(V)-13 b(AR)p
826 459 V 36 w(MA)i(TCHIDS)23 b(and)h(v)n(ariable)f(composition)e(with)
h(a)i(gi)n(v)o(en)e(array)i(of)g(ne)n(w)f(v)n(ariables.)-189
797 y Fo(3)143 b(CNF)35 b(Support)-189 1050 y Fj(3.1)119
b(F)m(ormat)-189 1237 y Fl(Gi)n(v)o(en)30 b(a)h(BDD)g(representing)g(a)
g(function)f Fd(f)11 b Fl(,)32 b(we)f(de)n(v)o(elop)f(three)h(basic)g
(possible)e(w)o(ays)i(to)g(store)f(it)h(as)g(a)g(CNF)-189
1358 y(formula.)54 b(In)33 b(each)h(method)d(the)i(set)g(of)f(clauses)h
(is)f(written)h(after)g(an)g(header)g(part.)55 b(Only)32
b(the)h(te)o(xt)f(format)g(is)-189 1478 y(allo)n(wed.)-189
1743 y Fi(3.1.1)99 b(Header)-189 1931 y Fl(The)23 b(header)h(part)f(of)
g(each)h(CNF)g(\002le)f(has)g(basically)g(the)f(same)h(format)g
(analyzed)g(for)h(the)f(BDD/ADD)g(\002les.)30 b(F)o(or)-189
2051 y(e)o(xample)h(the)g Fg(.rootids)f Fl(line)h(indicates)f(the)i(be)
o(ginning)d(of)j(each)g(CNF)g(formula)f(represented)h(by)f(a)h(single)
-189 2172 y(BDD.)j(T)-8 b(o)34 b(be)g(compatible)f(with)h(the)g(DIMA)l
(CS)h(format)f(each)h(header)f(line)g(start)g(with)g(the)g(character)h
(\223c\224)g(to)-189 2292 y(indicate)24 b(a)h(comment.)-189
2557 y Fi(3.1.2)99 b(T)-9 b(ext)25 b(F)n(ormat)-189 2745
y Fl(The)j(\002rst)g(method,)g(which)f(we)h(call)g Fi(Single-Node-Cut)p
Fl(,)j(models)26 b(each)j(BDD)f(nodes,)h(b)n(ut)e(the)h(ones)f(with)h
(both)-189 2865 y(the)c(children)g(equal)h(to)f(the)g(constant)g(node)g
Fb(1)p Fl(,)g(as)h(a)g(multiple)o(x)o(er)-5 b(.)27 b(Each)e(multiple)o
(x)o(er)d(has)i(tw)o(o)g(data)h(inputs)e(\(i.e.,)-189
2985 y(the)k(node)h(children\),)f(a)h(selection)f(input)f(\(i.e.,)i
(the)g(node)f(v)n(ariable\))g(and)h(one)f(output)f(\(i.e.,)i(the)g
(function)e(v)n(alue\))-189 3106 y(whose)h(v)n(alue)f(is)h(assigned)f
(to)h(an)g(additional)f(CNF)i(v)n(ariable.)37 b(The)27
b(\002nal)h(number)e(of)h(v)n(ariables)g(is)f(equal)h(to)g(the)-189
3226 y(number)d(of)h(original)f(BDD)h(v)n(ariables)f(plus)g(the)h
(number)f(of)h(\223internal\224)g(nodes)f(of)h(the)g(BDD.)47
3346 y(The)k(second)f(method,)g(which)h(we)f(call)h Fi(Maxterm-Cut)p
Fl(,)h(create)g(clauses)e(starting)g(from)g Fd(f)39 b
Fl(corresponds)-189 3467 y(to)25 b(the)h(of)n(f-set)g(\(i.e.,)f(all)h
(the)g(paths-cubes)f(from)g(the)h(root)g(node)f(to)h(the)f(terminal)g
Fg(0)p Fl(\))h(of)g(the)g(function)e Fd(f)11 b Fl(.)34
b(W)l(ithin)-189 3587 y(the)29 b(BDD)g(for)g Fd(f)11
b Fl(,)30 b(such)f(clauses)f(are)i(found)e(by)h(follo)n(wing)e(all)i
(the)f(paths)h(from)f(the)h(root)g(node)f(of)h(the)g(BDD)g(to)-189
3708 y(the)c(constant)f(node)g Fb(0)p Fl(.)31 b(The)25
b(\002nal)g(number)f(of)h(v)n(ariables)f(is)g(equal)h(to)f(the)h
(number)f(of)h(original)f(BDD)h(v)n(ariables.)47 3828
y(The)k(third)g(method,)g(which)g(we)g(call)g Fi(A)-5
b(uxiliary-V)c(ariable-Cut)p Fl(,)30 b(is)f(a)h(trade-of)n(f)f(between)
g(the)g(\002rst)g(tw)o(o)-189 3948 y(strate)o(gies.)69
b(Internal)37 b(v)n(ariables,)j(i.e.,)h(cutting)c(points,)j(are)e
(added)g(in)f(order)h(to)g(decompose)f(the)h(BDD)g(into)-189
4069 y(multiple)27 b(sub-trees)i(each)h(of)f(which)f(is)h(stored)g
(follo)n(wing)e(the)h(second)h(strate)o(gy)-6 b(.)42
b(The)29 b(trade-of)n(f)g(is)g(guided)f(by)-189 4189
y(the)23 b(cutting)f(point)g(selection)g(strate)o(gy)-6
b(,)22 b(and)h(we)g(e)o(xperiment)f(with)g(tw)o(o)g(methodologies.)28
b(In)23 b(the)g(\002rst)g(method,)g(a)-189 4310 y(ne)n(w)f(CNF)h(v)n
(ariable)f(is)f(inserted)h(in)g(correspondence)g(to)g(the)g(shared)g
(nodes)g(of)g(the)h(BDD,)f(i.e.,)h(the)f(nodes)f(which)-189
4430 y(ha)n(v)o(e)29 b(more)g(than)h(one)f(incoming)f(edge.)45
b(This)29 b(technique,)h(albeit)e(optimizing)g(the)h(number)g(of)h
(literals)e(stored,)-189 4550 y(can)35 b(produce)g(clauses)f(with)g(a)h
(high)f(number)h(of)f(literals)1894 4514 y Fh(2)1933
4550 y Fl(.)60 b(T)-8 b(o)35 b(a)n(v)n(oid)f(this)g(dra)o(wback,)j(the)
e(second)f(method,)-189 4671 y(introduces)28 b(all)g(the)g(pre)n
(viously)e(indicated)i(cutting)f(points)g(more)h(the)h(ones)f
(necessary)g(to)g(break)h(the)f(length)g(of)-189 4791
y(the)d(path)f(to)h(a)g(maximum)e(\(user\))i(selected)g(v)n(alue.)47
4911 y(Actually)-6 b(,)37 b(all)f(the)f(methods)g(described)h(abo)o(v)o
(e)e(can)j(be)e(re-conducted)h(to)g(the)f(basic)h(idea)g(of)g(possibly)
-189 5032 y(breaking)24 b(the)h(BDD)g(through)f(the)g(use)h(of)f
(additional)g(cutting)f(v)n(ariables)h(and)h(dumping)e(the)h(paths)g
(between)h(the)-189 5152 y(root)34 b(of)h(the)f(BDD,)h(the)g(cutting)e
(v)n(ariables)h(and)g(the)h(terminal)e(nodes.)60 b(Such)35
b(internal)f(cutting)f(v)n(ariables)h(are)-189 5273 y(added)25
b(al)o(w)o(ays)f(\(for)i(each)f(node\),)g(ne)n(v)o(er)f(or)h(sometimes)
e(respecti)n(v)o(ely)-6 b(.)p -189 5360 1607 4 v -77
5422 a Ff(2)-40 5452 y Fe(This)27 b(v)n(alue)f(is)i(superiorly)d
(limited)h(by)g(the)h(number)e(of)h(v)n(ariables)g(of)g(the)h(BDD,)g
(i.e.,)h(the)f(longest)f(path)g(from)g(the)h(root)f(to)g(the)-189
5551 y(terminal)19 b(node.)1794 5800 y Fl(7)p eop
%%Page: 8 8
8 7 bop 47 218 a Fl(While)33 b(the)f Fc(Single-Node-Cut)h
Fl(method)f(minimizes)f(the)i(length)f(of)h(the)f(clauses)h(produced,)i
(b)n(ut)d(it)g(also)-189 338 y(requires)d(the)h(higher)f(number)g(of)g
(CNF)i(v)n(ariables,)e(the)h Fc(Maxterm-Cut)f Fl(technique)g(minimizes)
f(the)h(number)g(of)-189 459 y(CNF)36 b(v)n(ariables)d(required.)61
b(This)34 b(adv)n(antage)g(is)g(counter)n(-balanced)h(by)f(the)h(f)o
(act)g(that)f(in)g(the)h(w)o(orst)f(case)h(the)-189 579
y(number)23 b(of)g(clauses,)g(as)h(well)e(as)i(the)f(total)f(number)h
(of)g(literals,)g(produced)g(is)g(e)o(xponential)e(in)i(the)g(BDD)h
(size)f(\(in)-189 699 y(terms)28 b(of)i(number)e(of)h(nodes\).)43
b(The)29 b(application)f(of)h(this)f(method)g(is)g(then)h(limited)e(to)
i(the)g(cases)g(in)f(which)h(the)-189 820 y(\223of)n(f-set\224)c(of)f
(the)g(represented)h(function)f Fd(f)35 b Fl(has)24 b(a)h(small)f
(cardinality)-6 b(.)29 b(The)c Fc(A)n(uxiliary-V)-11
b(ariable-Cut)22 b Fl(strate)o(gy)h(is)-189 940 y(a)k(trade-of)n(f)h
(between)f(the)g(\002rst)g(tw)o(o)g(methods)f(and)h(the)g(ones)f(which)
h(gi)n(v)o(es)f(more)h(compact)f(results.)37 b(As)27
b(a)h(\002nal)-189 1061 y(remark)f(notice)e(that)h(the)g(method)g(is)f
(able)i(to)f(store)g(both)f(monolithic)f(BDDs)j(and)f(conjuncti)n(v)o
(e)e(forms.)35 b(In)26 b(each)-189 1181 y(case)f(we)g(generate)h(CNF)f
(\002les)g(using)f(the)h(standard)f(DIMA)l(CS)i(format.)-189
1365 y Fi(Example)f(1)49 b Fc(F)l(igur)l(e)20 b(1)h(shows)f(an)h(e)n
(xample)g(of)f(how)h(our)f(pr)l(ocedur)l(e)h(works)f(to)h(stor)l(e)f(a)
h(small)f(monolithic)f(BDD.)-189 1486 y(F)l(igur)l(e)j(1\(a\))h(r)l
(epr)l(esents)g(a)g(BDD)g(with)g Fb(4)g Fc(nodes.)30
b(BDD)23 b(variables)f(ar)l(e)h(named)g(after)f(inte)l(g)o(er)g(number)
o(s)h(r)o(anging)-189 1606 y(fr)l(om)k Fb(1)h Fc(to)g
Fb(4)p Fc(,)h(to)f(have)g(an)g(easy-to-follow)f(corr)l(espondence)h
(with)g(the)g(CNF)h(variables.)40 b(F)l(igur)l(e)27 b(1\(b\),)i(\(c\))g
(and)-189 1727 y(\(d\))c(show)g(the)f(corr)l(esponding)f(CNF)j(r)l(epr)
l(esentations)d(g)o(ener)o(ated)h(by)h(our)f(thr)l(ee)h(methods.)30
b(As)24 b(in)h(the)f(standar)l(d)-189 1847 y(format)i
Fa(p)i Fc(indicates)e(the)h(total)f(number)g(of)h(variables)f(used)h
(\()p Fb(4)g Fc(is)g(the)g(minimum)f(value)h(as)g(the)g(BDD)g(itself)f
(has)-189 1967 y Fb(4)f Fc(variables\),)e(and)i Fa(cnf)g
Fc(the)f(total)g(number)g(of)h(clauses.)47 2088 y(As)i(a)g(\002nal)f(r)
l(emark)h(notice)f(that)g(for)g(this)g(speci\002c)h(e)n(xample)g(the)f
(\223Maxterm-Cut\224)i(appr)l(oac)o(h)d(is)h(the)h(one)-189
2208 y(whic)o(h)36 b(gives)g(the)g(most)f(compact)h(CNF)h(r)l(epr)l
(esentation)e(b)n(ut)h(also)f(the)h(clause)g(with)g(the)g(lar)l(g)o
(est)g(number)f(of)-189 2328 y(liter)o(als)23 b(\()p
Fb(4)p Fc(\).)188 2471 y
 6339814 10777681 0 0 11709153 19997655 startTexFig
 188 2471 a
%%BeginDocument: bdd.eps
%!PS-Adobe-2.0 EPSF-2.0
%%Title: bdd.eps
%%Creator: fig2dev Version 3.2 Patchlevel 3c
%%CreationDate: Mon Sep  9 14:21:26 2002
%%For: quer@pcsq (Stefano Quer)
%%BoundingBox: 0 0 178 304
%%Magnification: 1.0000
%%EndComments
/$F2psDict 200 dict def
$F2psDict begin
$F2psDict /mtrx matrix put
/col-1 {0 setgray} bind def
/col0 {0.000 0.000 0.000 srgb} bind def
/col1 {0.000 0.000 1.000 srgb} bind def
/col2 {0.000 1.000 0.000 srgb} bind def
/col3 {0.000 1.000 1.000 srgb} bind def
/col4 {1.000 0.000 0.000 srgb} bind def
/col5 {1.000 0.000 1.000 srgb} bind def
/col6 {1.000 1.000 0.000 srgb} bind def
/col7 {1.000 1.000 1.000 srgb} bind def
/col8 {0.000 0.000 0.560 srgb} bind def
/col9 {0.000 0.000 0.690 srgb} bind def
/col10 {0.000 0.000 0.820 srgb} bind def
/col11 {0.530 0.810 1.000 srgb} bind def
/col12 {0.000 0.560 0.000 srgb} bind def
/col13 {0.000 0.690 0.000 srgb} bind def
/col14 {0.000 0.820 0.000 srgb} bind def
/col15 {0.000 0.560 0.560 srgb} bind def
/col16 {0.000 0.690 0.690 srgb} bind def
/col17 {0.000 0.820 0.820 srgb} bind def
/col18 {0.560 0.000 0.000 srgb} bind def
/col19 {0.690 0.000 0.000 srgb} bind def
/col20 {0.820 0.000 0.000 srgb} bind def
/col21 {0.560 0.000 0.560 srgb} bind def
/col22 {0.690 0.000 0.690 srgb} bind def
/col23 {0.820 0.000 0.820 srgb} bind def
/col24 {0.500 0.190 0.000 srgb} bind def
/col25 {0.630 0.250 0.000 srgb} bind def
/col26 {0.750 0.380 0.000 srgb} bind def
/col27 {1.000 0.500 0.500 srgb} bind def
/col28 {1.000 0.630 0.630 srgb} bind def
/col29 {1.000 0.750 0.750 srgb} bind def
/col30 {1.000 0.880 0.880 srgb} bind def
/col31 {1.000 0.840 0.000 srgb} bind def

end
save
newpath 0 304 moveto 0 0 lineto 178 0 lineto 178 304 lineto closepath clip newpath
-51.0 319.0 translate
1 -1 scale

/cp {closepath} bind def
/ef {eofill} bind def
/gr {grestore} bind def
/gs {gsave} bind def
/sa {save} bind def
/rs {restore} bind def
/l {lineto} bind def
/m {moveto} bind def
/rm {rmoveto} bind def
/n {newpath} bind def
/s {stroke} bind def
/sh {show} bind def
/slc {setlinecap} bind def
/slj {setlinejoin} bind def
/slw {setlinewidth} bind def
/srgb {setrgbcolor} bind def
/rot {rotate} bind def
/sc {scale} bind def
/sd {setdash} bind def
/ff {findfont} bind def
/sf {setfont} bind def
/scf {scalefont} bind def
/sw {stringwidth} bind def
/tr {translate} bind def
/tnt {dup dup currentrgbcolor
  4 -2 roll dup 1 exch sub 3 -1 roll mul add
  4 -2 roll dup 1 exch sub 3 -1 roll mul add
  4 -2 roll dup 1 exch sub 3 -1 roll mul add srgb}
  bind def
/shd {dup dup currentrgbcolor 4 -2 roll mul 4 -2 roll mul
  4 -2 roll mul srgb} bind def
 /DrawEllipse {
	/endangle exch def
	/startangle exch def
	/yrad exch def
	/xrad exch def
	/y exch def
	/x exch def
	/savematrix mtrx currentmatrix def
	x y tr xrad yrad sc 0 0 1 startangle endangle arc
	closepath
	savematrix setmatrix
	} def

/$F2psBegin {$F2psDict begin /$F2psEnteredState save def} def
/$F2psEnd {$F2psEnteredState restore end} def

$F2psBegin
%%Page: 1 1
10 setmiterlimit
 0.06299 0.06299 sc
%
% Fig objects follow
%
% Polyline
15.000 slw
n 2010 4515 m 2550 4515 l 2550 5040 l 2010 5040 l
 cp gs col0 s gr 
/Times-Roman ff 300.00 scf sf
2205 4875 m
gs 1 -1 sc (1) col0 sh gr
% Ellipse
n 1515 1800 270 270 0 360 DrawEllipse gs col0 s gr

% Ellipse
n 2250 900 270 270 0 360 DrawEllipse gs col0 s gr

% Ellipse
n 2970 2715 270 270 0 360 DrawEllipse gs col0 s gr

% Ellipse
n 2280 3705 270 270 0 360 DrawEllipse gs col0 s gr

7.500 slw
% Ellipse
n 3555 3555 64 64 0 360 DrawEllipse gs 0.00 setgray ef gr gs col0 s gr

% Ellipse
n 2712 1726 64 64 0 360 DrawEllipse gs 0.00 setgray ef gr gs col0 s gr

% Ellipse
n 2430 4230 64 64 0 360 DrawEllipse gs 0.00 setgray ef gr gs col0 s gr

% Polyline
15.000 slw
n 2805 2910 m
 2250 3450 l gs col0 s gr 
% Polyline
 [90] 0 sd
gs  clippath
2940 2472 m 3010 2445 l 2931 2239 l 2957 2411 l 2861 2266 l cp
eoclip
n 2460 1110 m
 2970 2445 l gs col0 s gr gr
 [] 0 sd
% arrowhead
n 2861 2266 m 2957 2411 l 2931 2239 l 2908 2284 l 2861 2266 l 
 cp gs 0.00 setgray ef gr  col0 s
% Polyline
gs  clippath
1478 1511 m 1528 1568 l 1693 1422 l 1542 1506 l 1643 1366 l cp
eoclip
n 2025 1080 m
 1515 1530 l gs col0 s gr gr

% arrowhead
n 1643 1366 m 1542 1506 l 1693 1422 l 1643 1416 l 1643 1366 l 
 cp gs 0.00 setgray ef gr  col0 s
% Polyline
gs  clippath
2212 645 m 2287 645 l 2287 425 l 2250 594 l 2212 425 l cp
eoclip
n 2250 270 m
 2250 630 l gs col0 s gr gr

% arrowhead
n 2212 425 m 2250 594 l 2287 425 l 2250 459 l 2212 425 l 
 cp gs 0.00 setgray ef gr  col0 s
% Polyline
 [90] 0 sd
gs  clippath
2692 2664 m 2732 2601 l 2546 2485 l 2670 2606 l 2506 2548 l cp
eoclip
n 1710 2010 m
 2700 2625 l gs col0 s gr gr
 [] 0 sd
% arrowhead
n 2506 2548 m 2670 2606 l 2546 2485 l 2555 2534 l 2506 2548 l 
 cp gs 0.00 setgray ef gr  col0 s
% Polyline
2 slj
 [90] 0 sd
gs  clippath
2504 4653 m 2539 4720 l 2733 4616 l 2567 4663 l 2698 4550 l cp
eoclip
n 3180 2910 m 3181 2911 l 3183 2913 l 3186 2916 l 3192 2921 l 3200 2929 l
 3210 2939 l 3223 2951 l 3238 2966 l 3255 2984 l 3274 3003 l
 3295 3025 l 3317 3049 l 3339 3075 l 3362 3103 l 3385 3131 l
 3407 3161 l 3429 3192 l 3450 3225 l 3470 3258 l 3488 3293 l
 3504 3329 l 3519 3367 l 3531 3406 l 3541 3447 l 3548 3490 l
 3552 3536 l 3552 3583 l 3548 3634 l 3540 3686 l 3528 3740 l
 3510 3795 l 3490 3844 l 3467 3892 l 3441 3939 l 3413 3985 l
 3382 4028 l 3350 4070 l 3317 4110 l 3283 4148 l 3248 4184 l
 3211 4219 l 3174 4253 l 3136 4285 l 3098 4316 l 3059 4347 l
 3020 4376 l 2980 4405 l 2941 4432 l 2901 4459 l 2862 4484 l
 2824 4509 l 2787 4532 l 2751 4554 l 2717 4575 l 2686 4593 l
 2657 4610 l 2631 4626 l 2608 4639 l 2589 4650 l 2572 4659 l
 2559 4666 l 2550 4672 l
 2535 4680 l gs col0 s gr gr
 [] 0 sd
% arrowhead
0 slj
n 2698 4550 m 2567 4663 l 2733 4616 l 2686 4599 l 2698 4550 l 
 cp gs 0.00 setgray ef gr  col0 s
% Polyline
2 slj
gs  clippath
1985 4734 m 2028 4672 l 1847 4548 l 1965 4675 l 1804 4609 l cp
eoclip
n 1350 2025 m 1349 2026 l 1348 2027 l 1345 2030 l 1340 2035 l 1334 2042 l
 1325 2051 l 1314 2063 l 1301 2078 l 1286 2095 l 1268 2114 l
 1249 2137 l 1227 2161 l 1205 2188 l 1181 2218 l 1156 2249 l
 1131 2282 l 1105 2316 l 1080 2352 l 1054 2390 l 1029 2428 l
 1005 2468 l 981 2509 l 959 2552 l 938 2595 l 918 2640 l
 900 2687 l 884 2736 l 870 2786 l 858 2839 l 848 2894 l
 841 2951 l 837 3011 l 836 3074 l 838 3139 l 845 3206 l
 855 3275 l 870 3345 l 888 3412 l 910 3477 l 934 3542 l
 961 3604 l 990 3665 l 1022 3723 l 1054 3779 l 1088 3833 l
 1124 3885 l 1160 3935 l 1198 3983 l 1236 4029 l 1275 4074 l
 1315 4118 l 1356 4160 l 1397 4201 l 1438 4241 l 1480 4280 l
 1522 4318 l 1563 4355 l 1605 4390 l 1645 4424 l 1685 4457 l
 1723 4488 l 1760 4517 l 1795 4545 l 1827 4570 l 1857 4593 l
 1884 4613 l 1909 4632 l 1930 4647 l 1947 4660 l 1962 4671 l
 1973 4679 l 1982 4686 l
 1995 4695 l gs col0 s gr gr

% arrowhead
0 slj
n 1804 4609 m 1965 4675 l 1847 4548 l 1854 4598 l 1804 4609 l 
 cp gs 0.00 setgray ef gr  col0 s
% Polyline
2 slj
 [90] 0 sd
gs  clippath
2300 4492 m 2363 4532 l 2481 4347 l 2359 4470 l 2417 4307 l cp
eoclip
n 2340 3960 m 2341 3962 l 2344 3966 l 2348 3973 l 2354 3982 l 2362 3995 l
 2370 4010 l 2379 4028 l 2389 4046 l 2397 4066 l 2406 4088 l
 2413 4111 l 2420 4137 l 2425 4165 l 2429 4197 l 2430 4230 l
 2429 4263 l 2425 4295 l 2420 4323 l 2413 4349 l 2406 4372 l
 2397 4394 l 2389 4414 l 2379 4433 l 2370 4450 l 2362 4465 l
 2354 4478 l
 2340 4500 l gs col0 s gr gr
 [] 0 sd
% arrowhead
0 slj
n 2417 4307 m 2359 4470 l 2481 4347 l 2431 4356 l 2417 4307 l 
 cp gs 0.00 setgray ef gr  col0 s
% Polyline
2 slj
gs  clippath
2136 4532 m 2199 4492 l 2082 4307 l 2141 4470 l 2018 4347 l cp
eoclip
n 2160 3960 m 2159 3962 l 2156 3966 l 2152 3973 l 2146 3982 l 2138 3995 l
 2130 4010 l 2121 4028 l 2111 4046 l 2103 4066 l 2094 4088 l
 2087 4111 l 2080 4137 l 2075 4165 l 2071 4197 l 2070 4230 l
 2071 4263 l 2075 4295 l 2080 4323 l 2087 4349 l 2094 4372 l
 2103 4394 l 2111 4414 l 2121 4433 l 2130 4450 l 2138 4465 l
 2146 4478 l
 2160 4500 l gs col0 s gr gr

% arrowhead
0 slj
n 2018 4347 m 2141 4470 l 2082 4307 l 2068 4356 l 2018 4347 l 
 cp gs 0.00 setgray ef gr  col0 s
/Times-Roman ff 300.00 scf sf
2175 990 m
gs 1 -1 sc (1) col0 sh gr
/Times-Roman ff 300.00 scf sf
1440 1890 m
gs 1 -1 sc (2) col0 sh gr
/Times-Roman ff 300.00 scf sf
2895 2805 m
gs 1 -1 sc (3) col0 sh gr
/Times-Roman ff 300.00 scf sf
2205 3795 m
gs 1 -1 sc (4) col0 sh gr
$F2psEnd
rs

%%EndDocument

 endTexFig
 531 3990 a Fc(\(a\))1512 2504 y Fg(p)60 b(cnf)f(7)g(11)1512
2624 y(-5)g(3)h(0)1512 2745 y(-5)f(4)h(0)1512 2865 y(5)g(-3)f(-4)g(0)
1512 2985 y(6)h(-2)f(0)1512 3106 y(6)h(-5)f(0)1512 3226
y(-6)g(2)h(5)f(0)1512 3347 y(7)h(1)f(5)h(0)1512 3467
y(-7)f(1)h(-5)f(0)1512 3587 y(7)h(-1)f(-6)g(0)1512 3708
y(-7)g(-1)h(6)f(0)1512 3828 y(7)h(0)1836 3990 y Fc(\(b\))2541
2525 y Fg(p)f(cnf)g(4)h(3)2541 2645 y(1)f(-3)h(-4)f(0)2541
2766 y(-1)g(2)h(3)f(0)2541 2886 y(-1)g(2)h(-3)f(4)h(0)2868
3048 y Fc(\(c\))2541 3251 y Fg(p)f(cnf)g(5)h(5)2541 3371
y(-5)f(1)h(0)2541 3492 y(5)f(-1)h(2)f(0)2541 3612 y(-3)g(-4)g(5)h(0)
2541 3733 y(3)f(-5)h(0)2541 3853 y(-3)f(4)h(-5)f(0)2865
3990 y Fc(\(d\))-189 4138 y Fl(Figure)46 b(1:)71 b(\(a\))47
b(BDD;)e(\(b\))h(\223Single-Node-Cut\224)g(format;)55
b(\(c\))46 b(\223Maxterm-Cut\224)g(format;)55 b(\(d\))45
b(\223)-8 b(Auxiliary-)-189 4258 y(V)d(ariable-Cut\224)25
b(F)o(ormat.)-189 4625 y Fj(3.2)119 b(Implementation)-189
4813 y Fl(Store)25 b(and)g(Load)g(for)g(a)g(single)f(BDD)h(or)g(a)g
(forest)g(of)g(BDDs)g(is)f(currently)h(implemented.)-189
5073 y Fi(3.2.1)99 b(Storing)25 b(Decision)g(Diagrams)f(as)g(CNF)h(F)n
(ormulas)-189 5260 y Fl(As)g(f)o(ar)g(as)g(the)g(storing)e(process)i
(is)f(concerned)i(three)f(possible)e(formats)h(are)i(a)n(v)n(ailable:)
-44 5431 y Fk(\017)49 b Fl(DDDMP)p 421 5431 30 4 v 36
w(CNF)p 650 5431 V 36 w(MODE)p 980 5431 V 35 w(NODE:)21
b(store)f(a)h(BDD)h(by)e(introducing)f(an)i(auxiliary)g(v)n(ariable)f
(for)h(each)g(BDD)55 5551 y(node)1794 5800 y(8)p eop
%%Page: 9 9
9 8 bop -44 218 a Fk(\017)49 b Fl(DDDMP)p 421 218 30
4 v 36 w(CNF)p 650 218 V 36 w(MODE)p 980 218 V 35 w(MAXTERM:)20
b(store)g(a)h(BDD)h(by)e(follo)n(wing)f(the)h(maxterm)g(of)h(the)g
(represented)55 338 y(function)-44 542 y Fk(\017)49 b
Fl(DDDMP)p 421 542 V 36 w(CNF)p 650 542 V 36 w(MODE)p
980 542 V 35 w(BEST)-5 b(:)32 b(trade-of)f(between)h(the)f(tw)o(o)f
(pre)n(vious)g(solution,)h(trying)f(to)h(optimize)55
662 y(the)25 b(number)f(of)h(literals)f(stored.)-189
865 y(See)c(procedures)f(Dddmp)p 736 865 V 35 w(cuddBddStoreCnf)g(\(to)
g(store)f(a)h(single)f(BDD)i(as)e(a)i(CNF)f(formula\))g(and)g(Dddmp)p
3609 865 V 34 w(cuddBddArrayStoreCnf)-189 986 y(\(to)25
b(store)f(an)h(array)h(of)f(BDDs)g(as)f(a)i(CNF)f(formula\).)-189
1252 y Fi(3.2.2)99 b(Loadinf)26 b(CNF)e(F)n(ormulas)g(as)h(BDDs)-189
1439 y Fl(As)g(f)o(ar)g(as)g(the)g(loading)e(process)i(is)f(concerned)i
(three)f(possible)e(formats)i(are)g(a)n(v)n(ailable:)-44
1643 y Fk(\017)49 b Fl(DDDMP)p 421 1643 V 36 w(CNF)p
650 1643 V 36 w(MODE)p 980 1643 V 35 w(NO)p 1159 1643
V 36 w(CONJ:)25 b(Return)g(the)f(Clauses)h(without)f(Conjunction)-44
1846 y Fk(\017)49 b Fl(DDDMP)p 421 1846 V 36 w(CNF)p
650 1846 V 36 w(MODE)p 980 1846 V 35 w(NO)p 1159 1846
V 36 w(Q)o(U)l(ANT)-5 b(:)24 b(Return)h(the)g(sets)f(of)h(BDDs)g
(without)f(Quanti\002cation)-44 2050 y Fk(\017)49 b Fl(DDDMP)p
421 2050 V 36 w(CNF)p 650 2050 V 36 w(MODE)p 980 2050
V 35 w(CONJ)p 1264 2050 V 36 w(Q)o(U)l(ANT)-5 b(:)23
b(Return)h(the)g(sets)f(of)h(BDDs)g(AFTER)g(Existential)e(Quanti\002-)
55 2170 y(cation)-189 2373 y(See)e(procedures)f(Dddmp)p
736 2373 V 35 w(cuddBddLoadCnf)f(\(to)h(load)f(a)i(CNF)f(formula)g(as)g
(a)g(single)f(BDD\))h(and)g(Dddmp)p 3581 2373 V 35 w
(cuddBddArrayLoadCnf)-189 2494 y(\(to)35 b(load)h(a)g(CNF)g(formula)f
(as)h(an)g(array)g(of)g(BDDs\).)63 b(See)36 b(also)g(Dddmp)p
2485 2494 V 34 w(cuddHeaderLoadCnf)h(to)e(load)g(the)-189
2614 y(header)25 b(of)g(a)g(CNF)h(\002le)f(to)g(gather)f(information)f
(on)i(the)g(sa)n(v)o(ed)f(structure.)-189 2954 y Fo(4)143
b(T)-13 b(est)35 b(Pr)m(ogram)f(and)h(Regr)m(ession)f(T)-13
b(ests)-189 3177 y Fl(The)20 b Fc(testddmp.c)e Fl(\002le,)j(pro)o
(vided)d(with)h(this)f(distrib)n(ution,)g(e)o(x)o(empli\002es)g(some)h
(of)h(the)f(abo)o(v)o(e)g(features.)29 b(Moreo)o(v)o(er)l(,)-189
3298 y(in)d(the)h Fc(e)n(xp)g Fl(e)o(xperiments)e(a)j(fe)n(w)e
(scripts,)h(named)f Fc(test\241n\277.script)f Fl(are)i(a)n(v)n(ailable)
f(for)h(a)g(sanity)f(check)h(of)g(the)g(tool)-189 3418
y(and)e(to)f(tak)o(e)h(a)g(look)f(at)h(some)f(runs)h(e)o(x)o
(empli\002cation.)-189 3758 y Fo(5)143 b(Documentation)-189
3981 y Fl(F)o(or)27 b(further)f(documentation)f(on)i(the)f(package)h
(see)g(the)g(on-line)f(documentation)f(automatically)g(created)i(from)
-189 4102 y(the)e(source)g(code)g(\002les.)-189 4441
y Fo(6)143 b(Ackno)o(wledgments)-189 4665 y Fl(W)-8 b(e)19
b(are)h(particular)f(indebted)f(with)g(F)o(abio)g(Somenzi,)i(for)f
(discussions,)f(advice,)i(and)f(for)g(including)e(the)i(DDDMP)-189
4785 y(package)28 b(into)f(the)h(CUDD)g(distrib)n(ution.)37
b(W)-8 b(e)29 b(also)e(thank)g(all)h(the)g(user)g(of)g(the)f(package)i
(for)f(their)f(useful)h(indi-)-189 4905 y(cation)c(and)h(comments)f(on)
g(the)h(it.)1794 5800 y(9)p eop
%%Page: 10 10
10 9 bop -189 218 a Fo(7)143 b(FTP)35 b(Site)-189 441
y Fl(The)25 b(package)g(is)f(singularly)g(a)n(v)n(ailable)g(from:)-189
645 y Fg(site:)59 b(ftp.polito.it)-189 765 y(user:)g(anonymous)-189
885 y(directory:)f(/pub/research/dddmp)-189 1089 y Fl(or)25
b(directly)f(from)h(the)f(author)h(WEB)g(pages:)-189
1292 y Fg(WWW:)59 b(http://www.polito.it/\230{cabodi)o(,quer)o(})-189
1632 y Fo(8)143 b(F)l(eedback)-189 1855 y Fl(Send)25
b(feedback)h(to:)-189 2059 y Fg(Gianpiero)58 b(Cabodi)g(&)i(Stefano)e
(Quer)-189 2179 y(Politecnico)f(di)j(Torino)-189 2300
y(Dipartimento)d(di)i(Automatica)f(e)i(Informatica)-189
2420 y(Corso)f(Duca)g(degli)f(Abruzzi,)g(24)-189 2540
y(I-10129)g(Torino)-189 2661 y(Italy)-189 2781 y(E-mail:)g
({cabodi,quer}@polito.it)-189 2901 y(WWW:)h
(http://www.polito.it/\230{cabodi)o(,quer)o(})1769 5800
y Fl(10)p eop
%%Trailer
end
userdict /end-hook known{end-hook}if
%%EOF
